Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-03-14 11:28 559921a5

View on Github →

feat(algebra/category/Group): the free-forgetful adjunction for AddCommGroup (#2141)

feat(algebra/category/Group): the free-forgetful adjunction for AddCommGroup
fixes
Update src/group_theory/free_abelian_group.lean
oops

Estimated changes

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

added def AddCommGroup.adj

added def AddCommGroup.free

added theorem AddCommGroup.free_map_coe

added theorem AddCommGroup.free_obj_coe

Modified src/algebra/group/hom.lean

Modified src/group_theory/free_abelian_group.lean

added def free_abelian_group.hom_equiv

added theorem free_abelian_group.hom_equiv_apply

added theorem free_abelian_group.hom_equiv_symm_apply

deleted def free_abelian_group.lift.universal

added theorem free_abelian_group.lift_comp

added theorem free_abelian_group.map_of