Theorem CommGroup.equiv_prod_multiplicative_zmod

Modification history

2024-11-07 22:07
Mathlib/GroupTheory/FiniteAbelian/Basic.lean
feat(GroupTheory/FiniteAbelian/Duality): new file (#18738) …
Deleted CommGroup.equiv_prod_multiplicative_zmodView on Github →
2024-11-05 15:53
Mathlib/GroupTheory/FiniteAbelian.lean
multiplicative version of classification of finite abelian groups (#18659) …
Added CommGroup.equiv_prod_multiplicative_zmodView on Github →