OAI/RingTheory/Multiplicity/LechNatTrans.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.Lech.natTrans_homology_isoMod_of_iso line 23
  2. lemma OAI.Lech.bounded_natTrans_homology_isoMod line 37
  3. lemma OAI.Lech.Koszul.augmentation_naturality_source line 78
  4. lemma OAI.Lech.Koszul.complexQuotientπ_naturality line 95
  5. def OAI.Lech.Koszul.quotientAugmentationNat line 101
  6. lemma OAI.Lech.Koszul.quotientAugmentation_bounded line 120
  7. lemma OAI.Lech.Koszul.tensor_isZero_above line 138
  8. lemma OAI.Lech.Koszul.coneInr_isIso_at_top line 151
  9. lemma OAI.Lech.Koszul.inclusion_isIso_at_top line 159
  10. lemma OAI.Lech.Koszul.scalarCone_boundary_range line 172
  11. def OAI.Lech.Koszul.projectionTerm line 208
  12. lemma OAI.Lech.Koszul.inclusion_projectionTerm line 215
  13. lemma OAI.Lech.Koszul.projectionTerm_surjective line 225
  14. lemma OAI.Lech.Koszul.scalar_range_eq_ideal_smul line 231
  15. lemma OAI.Lech.Koszul.entryIdeal_cons_for_top line 238
  16. lemma OAI.Lech.Koszul.projectionTerm_boundary_range line 245
  17. lemma OAI.Lech.Koszul.projectionTerm_isIso_at_top line 262
  18. lemma OAI.Lech.Koszul.augmentation_f_at_top line 271
  19. lemma OAI.Lech.Koszul.shortComplex_homologyMap_iso_of_augmentation line 283
  20. lemma OAI.Lech.Koszul.quotientAugmentation_homology_top line 304
  21. lemma OAI.Lech.isIso_app_of_finite_retract line 366
  22. lemma OAI.Lech.basis_finite_retract line 394
  23. lemma OAI.Lech.isIso_app_of_finite_free line 405