Commit 2024-11-07 22:07 3113285d

View on Github →

feat(GroupTheory/FiniteAbelian/Duality): new file (#18738) This adds duality statements for finite abelian groups. It also fixes some docstrings and adds a missing namespace that was left out by accident in a previous PR,

Estimated changes

Modified Mathlib.lean

Modified Mathlib/GroupTheory/FiniteAbelian/Basic.lean

deleted theorem CommGroup.equiv_prod_multiplicative_zmod

added theorem CommGroup.equiv_prod_multiplicative_zmod_of_finite

Created Mathlib/GroupTheory/FiniteAbelian/Duality.lean

added theorem CommGroup.dvd_exponent

added theorem CommGroup.exists_apply_ne_one_aux

added theorem CommGroup.exists_apply_ne_one_of_hasEnoughRootsOfUnity

added theorem CommGroup.mulEquiv_monoidHom_of_hasEnoughRootsOfUnity

Modified Mathlib/RingTheory/RootsOfUnity/EnoughRootsOfUnity.lean

added theorem IsCyclic.monoidHom_equiv_self

deleted theorem monoidHom_equiv_self