OAI/AlgebraicGeometry/Seshadri/Divisors/OpenSectionsLinear.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MaximalSeshadri.Geometry.OpenSections line 19
2. instance OAI.MaximalSeshadri.Geometry.(instance at line 20) line 20
3. instance OAI.MaximalSeshadri.Geometry.(instance at line 22) line 22
4. def OAI.MaximalSeshadri.Geometry.freeOpenLinearEquiv line 33
5. def OAI.MaximalSeshadri.Geometry.openRestriction line 39
6. lemma OAI.MaximalSeshadri.Geometry.freeOpenLinearEquiv_naturality line 55