OAI/AlgebraicGeometry/Seshadri/Divisors/SectionCoefficientOrder.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MaximalSeshadri.Geometry.affineCoefficient line 17
2. lemma OAI.MaximalSeshadri.Geometry.affineCoefficient_change line 21
3. lemma OAI.MaximalSeshadri.Geometry.affineCoefficient_iso line 28
4. lemma OAI.MaximalSeshadri.Geometry.affineCoefficient_ne_zero line 53
5. lemma OAI.MaximalSeshadri.Geometry.coefficient_postcompose line 59
6. lemma OAI.MaximalSeshadri.Geometry.associated_unit_middle line 66
7. lemma OAI.MaximalSeshadri.Geometry.affineCoefficient_sectionMultiply line 71
8. lemma OAI.MaximalSeshadri.Geometry.affineCoefficient_power line 118
9. lemma OAI.MaximalSeshadri.Geometry.affineCoefficient_division line 134