OAI/AlgebraicGeometry/Seshadri/Divisors/SectionChart.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.MaximalSeshadri.Projective.projective_factor_open line 20
2. def OAI.MaximalSeshadri.Projective.sectionFrameOn line 38
3. lemma OAI.MaximalSeshadri.Projective.sectionFrameOn_coefficient line 44
4. lemma OAI.MaximalSeshadri.Projective.sectionFrameOn_normalized line 58
5. lemma OAI.MaximalSeshadri.Projective.sectionsMorphism_on line 63
6. lemma OAI.MaximalSeshadri.Projective.affine_coordinates_factor line 77
7. lemma OAI.MaximalSeshadri.Projective.evalAway_coordinate line 95
8. theorem OAI.MaximalSeshadri.Projective.sectionsMorphism_affine_equation line 106