Hopf problem: period family · period point

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

structure Mathoverflow1973.FullPeriodMatrix : Type

A full period matrix equipped with a nonvanishing determinant witness.

• matrix : Matrix (Fin 2) (Fin 2) ℂ

  The complex matrix underlying a full period matrix.

• nondegenerate : Function.Bijective ⇑(self.matrix.map Complex.im).mulVecLin