Theorem IsUnit.coe

Modification history

2026-03-07 11:26

Mathlib/Algebra/Group/Submonoid/Units.lean

feat(MulChar): generalize duality results on finite abelian groups to multiplicative characters (#33878)

Added IsUnit.coe View on Github →