Hopf problem: elliptic · core 7

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

def Mathoverflow1973.Elliptic.HigherHomology.fibreNormIndex : Kind → ℕ

The index contributed by the norm map for each elliptic fibre type.

Equations

• Mathoverflow1973.Elliptic.HigherHomology.fibreNormIndex Mathoverflow1973.Elliptic.Kind.three = 1
• Mathoverflow1973.Elliptic.HigherHomology.fibreNormIndex Mathoverflow1973.Elliptic.Kind.four = 2

theorem Mathoverflow1973.Elliptic.HigherHomology.fibreNormIndex_int_ne_zero (j : Kind) : ↑(fibreNormIndex j) ≠ 0