OAI/RingTheory/Multiplicity/KoszulQuotientFinite.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.Lech.Koszul.entryIdeal_powers_radical line 12
2. lemma OAI.Lech.Koszul.sup_entryIdeal_powers_radical line 27
3. def OAI.Lech.Koszul.quotient_scalar_zero line 31
4. lemma OAI.Lech.Koszul.quotient_tensor_annihilator line 38
5. lemma OAI.Lech.Koszul.finite_moduleQuotient line 48
6. lemma OAI.Lech.Koszul.single_terms_finite line 53
7. lemma OAI.Lech.Koszul.quotient_tensor_single_finiteLength line 61