OAI/AlgebraicGeometry/Seshadri/Geometry/PlaneCoordinates.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MaximalSeshadri.Projective.ratioOn line 17
2. lemma OAI.MaximalSeshadri.Projective.ratioOn_full line 21
3. lemma OAI.MaximalSeshadri.Projective.ratioOn_self line 27
4. def OAI.MaximalSeshadri.Projective.ratioUnitOn line 31
5. lemma OAI.MaximalSeshadri.Projective.ratioUnitOn_val line 36
6. lemma OAI.MaximalSeshadri.Projective.ratioOn_restrict line 44
7. lemma OAI.MaximalSeshadri.Projective.ratioUnitOn_restrict line 51
8. lemma OAI.MaximalSeshadri.Projective.ratioOn_cocycle line 60
9. lemma OAI.MaximalSeshadri.Projective.ratioUnitOn_cocycle line 68
10. lemma OAI.MaximalSeshadri.Projective.ratioUnitOn_symm line 76
11. lemma OAI.MaximalSeshadri.Projective.ratioOn_basicOpen line 82