OAI/NumberTheory/PiExponent/Geometry/ProjectiveSectionPullback.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.PiExponent.ProjectiveSectionExtension.globalPushEquiv line 13
2. def OAI.PiExponent.ProjectiveSectionExtension.quotientPowerIso line 19
3. def OAI.PiExponent.ProjectiveSectionExtension.quotientSectionsEquiv line 25
4. theorem OAI.PiExponent.ProjectiveSectionExtension.quotientSectionsEquiv_restriction line 32
5. theorem OAI.PiExponent.ProjectiveSectionExtension.eventual_projective_pullbackPowerSection_surjective line 50
6. theorem OAI.PiExponent.ProjectiveSectionExtension.eventual_projective_homogeneous_extension line 61