OAI/RingTheory/Multiplicity/LechQuotientScalar.lean

GitHub source file

32 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.Lech.quotientScalar line 22
  2. lemma OAI.Lech.basis_quotient_length line 26
  3. def OAI.Lech.finiteTorsionCechEuler line 38
  4. lemma OAI.Lech.pureCohomology_length line 40
  5. lemma OAI.Lech.pureCohomology_length_zero line 45
  6. lemma OAI.Lech.pureCohomology_length_finite line 49
  7. lemma OAI.Lech.pureCohomology_torsionEuler line 60
  8. theorem OAI.Lech.ProductSourceCover.rootTarget_length_finite line 84
  9. theorem OAI.Lech.ProductSourceCover.rootTarget_torsionEuler line 90
  10. def OAI.Lech.ComplexPi.tailMap line 115
  11. def OAI.Lech.ComplexPi.headMap line 121
  12. def OAI.Lech.ComplexPi.consZeroMap line 127
  13. def OAI.Lech.ComplexPi.consHeadMap line 140
  14. def OAI.Lech.ComplexPi.copiesShortComplex line 154
  15. def OAI.Lech.ComplexPi.copiesSplitting line 157
  16. lemma OAI.Lech.ComplexPi.copies_zero_isZero line 166
  17. lemma OAI.Lech.ComplexPi.copies_homology_property line 178
  18. lemma OAI.Lech.quotientScalar_powerTorsion line 192
  19. def OAI.Lech.quotientFiniteClass line 201
  20. instance OAI.Lech.(instance at line 203) line 203
  21. lemma OAI.Lech.ProductSourceCover.rootTwistRow_quotientFinite line 214
  22. theorem OAI.Lech.ProductSourceCover.rootLayerTotal_quotientFinite line 236
  23. def OAI.Lech.quotientLength line 264
  24. lemma OAI.Lech.quotientLength_finite_iff line 270
  25. lemma OAI.Lech.ComplexPi.copies_euler line 287
  26. lemma OAI.Lech.ProductSourceCover.rootTwistRow_length line 315
  27. lemma OAI.Lech.ProductSourceCover.rootTwistRow_euler line 331
  28. lemma OAI.Lech.ProductSourceCover.single_euler line 346
  29. lemma OAI.Lech.ProductSourceCover.rootDegree_le line 370
  30. lemma OAI.Lech.ProductSourceCover.rootLayerTerm_finite line 373
  31. lemma OAI.Lech.ProductSourceCover.rootLayerTerm_isZero line 383
  32. theorem OAI.Lech.ProductSourceCover.rootLayerTotal_euler_rows line 399