Mathlib v3 is deprecated. Go to Mathlib v4

Def mul_equiv.unique_prod

Modification history

2022-06-23 14:10
src/algebra/group/prod.lean
feat(group_theory/finite_abelian): Structure of finite abelian groups (#14736) …
Added mul_equiv.unique_prodView on Github →