Theorem FiniteMultiplicity.not_isUnit

Modification history

2026-08-03 08:23
Mathlib/RingTheory/Multiplicity.lean
chore: rename `FiniteMultiplicity.not_unit` to `FiniteMultiplicity.not_isUnit` (#42390)
Added FiniteMultiplicity.not_isUnitView on Github →