OAI/NumberTheory/PiExponent/Geometry/ProjectiveChartOverlaps.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.PiExponentSeshadri.Projective.openImmersionSectionIso_restrict line 11
2. lemma OAI.PiExponentSeshadri.Projective.coordinate_chart_preimage line 20
3. def OAI.PiExponentSeshadri.Projective.chartPairSectionRingEquiv line 30
4. lemma OAI.PiExponentSeshadri.Projective.coordinate_finset_preimage line 52
5. def OAI.PiExponentSeshadri.Projective.chartFiniteSectionRingEquiv line 64
6. def OAI.PiExponentSeshadri.Projective.chartFinitePolynomialRingEquiv line 85
7. def OAI.PiExponentSeshadri.Projective.chartVariableOverlapRingEquiv line 101