Mathlib v3 is deprecated. Go to Mathlib v4

Def mul_equiv.to_CommGroup_iso

Modification history

2022-03-04 09:26
src/algebra/category/Group/basic.lean
refactor(algebra/category/Group/basic): Avoid data shuffle in `mul_equiv.to_Group_iso` (#12407) …
Modified mul_equiv.to_CommGroup_isoView on Github →
2020-05-27 07:09
src/algebra/category/Group/basic.lean
chore(*): split long lines, unindent in namespaces (#2834) …
Modified mul_equiv.to_CommGroup_isoView on Github →
2019-11-12 13:20
src/algebra/category/Group.lean
feat(data/equiv,category_theory): prove equivalences are the same as isos (#1587) …
Added mul_equiv.to_CommGroup_isoView on Github →