Mathlib v3 is deprecated. Go to Mathlib v4

Theorem free_abelian_group.hom_equiv_symm_apply

Modification history

2021-02-20 21:09
src/group_theory/free_abelian_group.lean
refactor(group_theory/free_*): remove API duplicated by lift, promote lift functions to equivs (#6311) …
Deleted free_abelian_group.hom_equiv_symm_applyView on Github →
2020-03-14 11:28
src/group_theory/free_abelian_group.lean
feat(algebra/category/Group): the free-forgetful adjunction for AddCommGroup (#2141) …
Added free_abelian_group.hom_equiv_symm_applyView on Github →