OAI/NumberTheory/PiExponent/Geometry/CurveEffectiveTwist.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PiExponent.CurveDegree.id_eq_zero_of_iso line 15
2. theorem OAI.PiExponent.CurveDegree.generators_isZero line 20
3. theorem OAI.PiExponent.CurveDegree.lineBundle_not_isZero line 33
4. theorem OAI.PiExponent.CurveDegree.section_ne_zero_of_mem_isoOpen line 50
5. theorem OAI.PiExponent.CurveDegree.nonzero_section_of_generators line 63
6. def OAI.PiExponent.CurveDegree.twistLineIso line 70
7. theorem OAI.PiExponent.CurveDegree.exists_effective_twist line 75