Hopf problem: lattice · core 1

Supporting definitions and proofs for this stage of the six-sphere construction.

@[reducible, inline]

abbrev Mathoverflow1973.Lattice : Type

The rank-four integer lattice in coordinate form.

Equations

• Mathoverflow1973.Lattice = (Fin 4 → ℤ)