Mathlib Changelog
v4
Changelog
About
Github
Theorem
FiniteMultiplicity.lt_multiplicity_of_lt_emultiplicity
Modification history
2024-12-06 14:50
Mathlib/RingTheory/Multiplicity.lean
chore: eliminate `multiplicity` namespace (#19623)
Added
FiniteMultiplicity.lt_multiplicity_of_lt_emultiplicity
View on Github →