OAI/NumberTheory/PiExponent/Geometry/CurveNormalizationDimension.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.PiExponent.CurveNormalizationModel.parameterCurveOpenCover line 16
2. instance OAI.PiExponent.CurveNormalizationModel.parameterChart_noetherian line 34
3. instance OAI.PiExponent.CurveNormalizationModel.parameterCurve_noetherian line 43
4. theorem OAI.PiExponent.CurveNormalizationModel.parameterCurve_dimension_le_one line 57
5. theorem OAI.PiExponent.CurveNormalizationModel.parameterCurve_isClosed_of_ne_generic line 75
6. theorem OAI.PiExponent.CurveNormalizationModel.parameterCurve_exists_nongeneric line 96
7. theorem OAI.PiExponent.CurveNormalizationModel.parameterCurve_isClosed_iff_ne_generic line 119