OAI/NumberTheory/PiExponent/Geometry/ProjectiveFinitePencil.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.PiExponent.ProjectivePencil.lineBundle line 18
2. def OAI.PiExponent.ProjectivePencil.coordinateSection line 21
3. def OAI.PiExponent.ProjectivePencil.scalars line 25
4. theorem OAI.PiExponent.ProjectivePencil.sections_cover line 28
5. theorem OAI.PiExponent.ProjectivePencil.sectionsMorphism_eq line 32
6. instance OAI.PiExponent.ProjectivePencil.sectionsMorphism_isFinite line 41
7. theorem OAI.PiExponent.ProjectivePencil.H0_finite line 53
8. theorem OAI.PiExponent.ProjectivePencil.H1_finite line 60
9. theorem OAI.PiExponent.ProjectivePencil.scalars_eq_baseScalars line 71
10. theorem OAI.PiExponent.ProjectivePencil.H0_finite_complex line 76
11. theorem OAI.PiExponent.ProjectivePencil.H1_finite_complex line 85