OAI/NumberTheory/PiExponent/Cohomology/PencilCohomologyLaurent.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.PiExponentSeshadri.LaurentTails.positive_tail line 14
  2. lemma OAI.PiExponentSeshadri.LaurentTails.negative_tail line 25
  3. theorem OAI.PiExponentSeshadri.LaurentTails.quotient_finite line 35
  4. theorem OAI.PiExponentSeshadri.LaurentCech.cokernel_finite line 104
  5. instance OAI.PiExponentSeshadri.LaurentLattices.(instance at line 163) line 163
  6. def OAI.PiExponentSeshadri.LaurentLattices.boundedBelow line 170
  7. def OAI.PiExponentSeshadri.LaurentLattices.boundedAbove line 176
  8. lemma OAI.PiExponentSeshadri.LaurentLattices.mem_boundedBelow line 185
  9. lemma OAI.PiExponentSeshadri.LaurentLattices.mem_boundedAbove line 192
  10. lemma OAI.PiExponentSeshadri.LaurentLattices.coeff_T_mul line 199
  11. lemma OAI.PiExponentSeshadri.LaurentLattices.below_shift line 205
  12. lemma OAI.PiExponentSeshadri.LaurentLattices.above_shift line 213
  13. theorem OAI.PiExponentSeshadri.LaurentLattices.band_finite line 221
  14. lemma OAI.PiExponentSeshadri.LaurentLattices.finite_generators_bounded line 242
  15. theorem OAI.PiExponentSeshadri.LaurentLattices.intersection_finite line 265
  16. instance OAI.PiExponentSeshadri.LaurentLattices.laurent_finiteType line 294
  17. lemma OAI.PiExponentSeshadri.LaurentLattices.quotient_finite line 303
  18. theorem OAI.PiExponentSeshadri.LaurentLattices.torsion_finite line 312
  19. theorem OAI.PiExponentSeshadri.LaurentLattices.intersection_finite_general line 336
  20. lemma OAI.PiExponentSeshadri.LaurentLattices.range_le_lattice line 389
  21. theorem OAI.PiExponentSeshadri.LaurentLattices.range_intersection_finite line 408
  22. theorem OAI.PiExponentSeshadri.LaurentCech.intersection_finite line 448