OAI/NumberTheory/PiExponent/Geometry/ProjectiveChartRingNaturality.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.PiExponentSeshadri.Projective.relabeledOverlapEquiv line 13
2. lemma OAI.PiExponentSeshadri.Projective.relabeledOverlapEquiv_restrict line 20
3. lemma OAI.PiExponentSeshadri.Projective.chartVariableOverlapRingEquiv_restrict line 31
4. lemma OAI.PiExponentSeshadri.Projective.chartVariableOverlapRingEquiv_restrict_chart line 56
5. lemma OAI.PiExponentSeshadri.Projective.chartVariableOverlapRingEquiv_restrict_coordinate line 67
6. lemma OAI.PiExponentSeshadri.Projective.chartVariableOverlapRingEquiv_restrict_constant line 76
7. lemma OAI.PiExponentSeshadri.Projective.chartVariableOverlapRingEquiv_restriction_algebraMap line 84