OAI/NumberTheory/PiExponent/Geometry/CurveNormalizationUnit.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.PiExponent.CurveNormalizationDegree.unitMap line 12
2. theorem OAI.PiExponent.CurveNormalizationDegree.unitMap_mono line 16
3. theorem OAI.PiExponent.CurveNormalizationDegree.dominant_of_iso_restrict line 25
4. theorem OAI.PiExponent.CurveNormalizationDegree.unitMap_restrict_isIso line 38
5. theorem OAI.PiExponent.CurveNormalizationDegree.unitMap_isoOpen_ne_bot line 54
6. def OAI.PiExponent.CurveNormalizationDegree.pushforwardPullbackIso line 62