OAI/RingTheory/Multiplicity/FiniteFreeRetract.lean
3 declarations, 0 contain sorry, 0 declared as axioms
- lemma
OAI.Lech.finite_free_retractline 12 - lemma
OAI.Lech.isZero_of_retractline 24 - lemma
OAI.Lech.null_projector_contractible_splittingline 30