Group): the free-forgetful adjunction for AddCommGroup
#2141

Merged

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

mergify merged 6 commits into master from AddCommGroup_forget_adjunction

feat(algebra/category/Group): the free-forgetful adjunction for AddCo…

52af4127

fixes

8ed3f8f1

jcommelin approved these changes on 2020-03-13

Update src/group_theory/free_abelian_group.lean

c4654a14

jcommelin requested a review from

jcommelin 6 years ago

oops

b8b77211

kim-em added awaiting-review

jcommelin approved these changes on 2020-03-14

jcommelin removed awaiting-review

jcommelin added ready-to-merge

Merge branch 'master' into AddCommGroup_forget_adjunction

a8ea9ae5

Merge branch 'master' into AddCommGroup_forget_adjunction

bdec4255

mergify merged 559921a5 into master 6 years ago

mergify deleted the AddCommGroup_forget_adjunction branch 6 years ago

Reviewers

jcommelin

Assignees

No one assigned

Labels

ready-to-merge

Milestone

No milestone