OAI/RingTheory/Multiplicity/AdditiveLength.lean
2 declarations, 0 contain sorry, 0 declared as axioms
- lemma
OAI.Lech.additive_length_piline 12 - lemma
OAI.Lech.additive_length_finite_freeline 20
OAI/RingTheory/Multiplicity/AdditiveLength.lean2 declarations, 0 contain sorry, 0 declared as axioms
OAI.Lech.additive_length_pi line 12OAI.Lech.additive_length_finite_free line 20