Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-02-15 03:01 c94577a6

View on Github →

feat(group_theory/free_abelian_group): add module doc and some equivs (#6062) Also add some API for free_abelian_group.map.

Estimated changes

Modified src/algebra/category/Group/adjunctions.lean

Modified src/group_theory/free_abelian_group.lean

added def free_abelian_group.equiv_of_equiv

added theorem free_abelian_group.map_comp

added theorem free_abelian_group.map_comp_apply

added theorem free_abelian_group.map_id

added theorem free_abelian_group.map_id_apply

added theorem free_abelian_group.map_of_apply

added def free_abelian_group.punit_equiv