Commit 2026-08-03 08:23 c10d9bc1

View on Github →

chore: rename FiniteMultiplicity.not_unit to FiniteMultiplicity.not_isUnit (#42390)

Estimated changes

Modified Mathlib/RingTheory/Multiplicity.lean

added theorem FiniteMultiplicity.not_isUnit

deleted theorem FiniteMultiplicity.not_unit