Commit 2026-02-26 19:49 b5ae6ec9

View on Github →

feat(GroupTheory/FiniteAbelian): construct bijection between subgroups and subgroups of the dual (#33792)

Estimated changes

Modified Mathlib/GroupTheory/FiniteAbelian/Duality.lean

added theorem CommGroup.apply_monoidHomMonoidHomEquiv

added theorem CommGroup.forall_apply_eq_apply_iff

added theorem CommGroup.forall_monoidHom_apply_eq_one_iff

added theorem CommGroup.mem_subgroupOrderIsoSubgroupMonoidHom_iff

added theorem CommGroup.mem_subgroupOrderIsoSubgroupMonoidHom_symm_iff

modified theorem MonoidHom.restrict_surjective

Modified Mathlib/RingTheory/RootsOfUnity/EnoughRootsOfUnity.lean