Commit 2025-11-25 14:31 a7a662d2

View on Github →

feat(Algebra): more instances of subsingleton units (#26110) Add some missing instances of Subsingleton Mˣ. From Toric

Estimated changes

Modified Mathlib/Algebra/Group/Pi/Units.lean

Modified Mathlib/Algebra/Group/Prod.lean

Modified Mathlib/Algebra/Group/Submonoid/Units.lean

Modified Mathlib/Algebra/Group/Units/Basic.lean

deleted theorem units_eq_one

Modified Mathlib/Algebra/Group/Units/Defs.lean

added theorem IsUnit.eq_one

added theorem Subsingleton.units_of_isUnit

added theorem Units.eq_one

modified theorem isUnit_iff_eq_one

Modified Mathlib/Algebra/GroupWithZero/Associated.lean

Modified Mathlib/Data/ZMod/Basic.lean

Modified Mathlib/NumberTheory/DirichletCharacter/Basic.lean