OAI/AlgebraicGeometry/Seshadri/Cohomology/LaurentLattices.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. instance OAI.MaximalSeshadri.LaurentLattices.(instance at line 16) line 16
2. def OAI.MaximalSeshadri.LaurentLattices.boundedBelow line 23
3. def OAI.MaximalSeshadri.LaurentLattices.boundedAbove line 29
4. lemma OAI.MaximalSeshadri.LaurentLattices.mem_boundedBelow line 38
5. lemma OAI.MaximalSeshadri.LaurentLattices.mem_boundedAbove line 45
6. lemma OAI.MaximalSeshadri.LaurentLattices.coeff_T_mul line 52
7. lemma OAI.MaximalSeshadri.LaurentLattices.below_shift line 58
8. lemma OAI.MaximalSeshadri.LaurentLattices.above_shift line 66
9. theorem OAI.MaximalSeshadri.LaurentLattices.band_finite line 74
10. lemma OAI.MaximalSeshadri.LaurentLattices.finite_generators_bounded line 95
11. theorem OAI.MaximalSeshadri.LaurentLattices.intersection_finite line 118