OAI/RingTheory/Multiplicity/SumEstimate.lean
2 declarations, 0 contain sorry, 0 declared as axioms
- lemma
OAI.Lech.ReesRoot.quotient_root_eulerline 32 - theorem
OAI.Lech.ReesRoot.sum_estimateline 70
OAI/RingTheory/Multiplicity/SumEstimate.lean2 declarations, 0 contain sorry, 0 declared as axioms
OAI.Lech.ReesRoot.quotient_root_euler line 32OAI.Lech.ReesRoot.sum_estimate line 70