OAI/RingTheory/Multiplicity/KoszulFiniteComplexBound.lean
2 declarations, 0 contain sorry, 0 declared as axioms
- lemma
OAI.Lech.Koszul.length_quotient_tensor_le_sumline 12 - theorem
OAI.Lech.Koszul.length_quotient_le_koszul_powersline 37