Hopf problem: uniformization · special periods 3

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

theorem Mathoverflow1973.SpecialPeriods.analyticOrderAt_E₆_of_eq_zero (z : UpperHalfPlane) (hz : ModularForm.E₆ z = 0) : analyticOrderAt (⇑ModularForm.E₆ ∘ ↑UpperHalfPlane.ofComplex) ↑z = 1