OAI/NumberTheory/PiExponent/Geometry/ProjectiveCoordinateRingNaturality.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.PiExponentSeshadri.Projective.isoPreimageSectionRingEquiv_symm line 9
2. lemma OAI.PiExponentSeshadri.Projective.isoPreimageSectionRingEquiv_appLE line 18
3. lemma OAI.PiExponentSeshadri.Projective.appLE_restrict_comm line 26
4. lemma OAI.PiExponentSeshadri.Projective.coordinateSectionChartIso_factor line 41
5. lemma OAI.PiExponentSeshadri.Projective.coordinateSectionChartIso_pullback line 52
6. lemma OAI.PiExponentSeshadri.Projective.coordinateSectionRingEquiv_symm line 65
7. lemma OAI.PiExponentSeshadri.Projective.coordinateFiniteRingEquiv_appLE line 74
8. lemma OAI.PiExponentSeshadri.Projective.coordinateFiniteRingEquiv_restrict line 88