Hopf problem: elliptic · core 1

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

inductive Mathoverflow1973.Elliptic.Kind : Type

The two elliptic fibre types, distinguished by monodromy order three or four.

• three : Kind
• four : Kind

@[instance_reducible]

instance Mathoverflow1973.Elliptic.instDecidableEqKind : DecidableEq Kind

Equations

• Mathoverflow1973.Elliptic.instDecidableEqKind x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯