OAI/NumberTheory/PiExponent/Geometry/ProjectiveSectionInterface.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.PiExponent.ProjectiveSectionInterface.sectionHom line 14
2. def OAI.PiExponent.ProjectiveSectionInterface.ofSectionHom line 17
3. theorem OAI.PiExponent.ProjectiveSectionInterface.sectionHom_ofSectionHom line 21
4. theorem OAI.PiExponent.ProjectiveSectionInterface.ofSectionHom_sectionHom line 26
5. theorem OAI.PiExponent.ProjectiveSectionInterface.sectionHom_injective line 29
6. def OAI.PiExponent.ProjectiveSectionInterface.pullback line 32
7. theorem OAI.PiExponent.ProjectiveSectionInterface.sectionHom_pullback line 37
8. theorem OAI.PiExponent.ProjectiveSectionInterface.eventual_homogeneous_extension line 45