Theorem FiniteMultiplicity.one_right

Modification history

2026-09-11 16:02
Mathlib/RingTheory/Multiplicity.lean
chore(RingTheory/Multiplicity): generalize API (#43716) …
Deleted FiniteMultiplicity.one_rightView on Github →
2024-12-06 14:50
Mathlib/RingTheory/Multiplicity.lean
chore: eliminate `multiplicity` namespace (#19623)
Added FiniteMultiplicity.one_rightView on Github →