Commit 2026-03-07 11:26 9c26b87a

View on Github →

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

Estimated changes

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

added theorem IsUnit.coe

Modified Mathlib/NumberTheory/MulChar/Basic.lean

deleted def MulChar.mulEquivToUnitHom

added theorem MulChar.restrict_eq_one_iff

Modified Mathlib/NumberTheory/MulChar/Duality.lean

added theorem MulChar.apply_mulCharEquiv

added theorem MulChar.mem_subgroupOrderIsoSubgroupMulChar_iff

added theorem MulChar.mem_subgroupOrderIsoSubgroupMulChar_symm_iff

added theorem MulChar.mulCharEquiv_symm_apply_apply

added theorem MulChar.restrictHom_surjective

Modified Mathlib/NumberTheory/MulChar/Lemmas.lean

modified theorem MulChar.eq_iff

added theorem MulChar.restrict_ofUnitHom