OAI/RingTheory/Multiplicity/KoszulTensorSingle.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Lech.Koszul.tensorSingleHomologyIso line 23
  2. lemma OAI.Lech.Koszul.augmentation_scalar_isoMod line 46
  3. lemma OAI.Lech.Koszul.augmentation_free_isoMod line 75
  4. lemma OAI.Lech.Koszul.augmentation_finiteFree_bounded_isoMod line 94
  5. lemma OAI.Lech.monoModSerre_of_comp line 113
  6. lemma OAI.Lech.isIso_of_image_factorizations line 122
  7. lemma OAI.Lech.cofinal_stableImage_isoMod line 138
  8. lemma OAI.Lech.sup_pow_add_pred_le line 181
  9. lemma OAI.Lech.finset_sup_pow_le line 194
  10. lemma OAI.Lech.parameter_power_cofinality line 210
  11. lemma OAI.Lech.entryIdeal_power_antitone line 231
  12. lemma OAI.Lech.quotientAugmentation_power_naturality line 241
  13. lemma OAI.Lech.koszul_stableImage_isIso line 267
  14. lemma OAI.Lech.parameterPower_stableImage_isoMod line 284
  15. lemma OAI.Lech.entryIdeal_ofFn line 331
  16. lemma OAI.Lech.parameterPower_source_monoMod line 338
  17. lemma OAI.Lech.complexQuotientMap_comp line 359
  18. lemma OAI.Lech.ordinaryPower_stableImage_isoMod line 368