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

Commit
5 years ago
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 Co-authored-by: Johan Commelin <johan@commelin.net> Co-authored-by: mergify[bot] <37929162+mergify[bot]@users.noreply.github.com>
Author
Parents
Loading