OAI/NumberTheory/PiExponent/Ampleness/AffineFunctionFieldCompatibility.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PiExponent.CurveNormalizationModel.isFractionRing_of_intermediate_domain line 13
2. def OAI.PiExponent.CurveNormalizationModel.affineFunctionFieldEquiv line 32
3. theorem OAI.PiExponent.CurveNormalizationModel.affineFunctionFieldEquiv_toStalk line 39
4. theorem OAI.PiExponent.CurveNormalizationModel.affineFunctionFieldEquiv_stalk line 49
5. theorem OAI.PiExponent.CurveNormalizationModel.affineFunctionFieldEquiv_naturality line 83