Hopf problem: foundations · core 2

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

@[reducible, inline]

abbrev Mathoverflow1973.ComplexPlane₂ : Type

The two-dimensional complex coordinate space.

Equations

• Mathoverflow1973.ComplexPlane₂ = (Fin 2 → ℂ)

@[reducible, inline]

abbrev Mathoverflow1973.RealPlane₄ : Type

The four-dimensional real coordinate space underlying ComplexPlane₂.

Equations

• Mathoverflow1973.RealPlane₄ = (Fin 4 → ℝ)