Mathlib v3 is deprecated. Go to Mathlib v4

Def equiv.prod_unique

Modification history

2022-06-23 14:10

src/logic/equiv/basic.lean

feat(group_theory/finite_abelian): Structure of finite abelian groups (#14736) …

Added equiv.prod_unique View on Github →