OAI/RingTheory/Multiplicity/TensorCoefficientFibre.lean
3 declarations, 0 contain sorry, 0 declared as axioms
- lemma
OAI.Lech.TensorIdeal.map_ideal_smul_topline 16 - def
OAI.Lech.TensorIdeal.quotientUnitTensorEquivline 24 - lemma
OAI.Lech.TensorIdeal.quotientUnitTensorEquiv_mkline 29