Theorem CommGroup.equiv_prod_multiplicative_zmod_of_finite

Modification history

2024-11-07 22:07
Mathlib/GroupTheory/FiniteAbelian/Basic.lean
feat(GroupTheory/FiniteAbelian/Duality): new file (#18738) …
Added CommGroup.equiv_prod_multiplicative_zmod_of_finiteView on Github →