OAI/RingTheory/Multiplicity/ComplexReduction.lean
4 declarations, 0 contain sorry, 0 declared as axioms
- def
OAI.Lech.TensorIdeal.complexQuotientNatline 13 - lemma
OAI.Lech.TensorIdeal.complexQuotientNat_fline 18 - def
OAI.Lech.TensorIdeal.bicomplexQuotientNatline 24 - lemma
OAI.Lech.TensorIdeal.bicomplexQuotientNat_fline 30