Mathlib v3 is deprecated. Go to Mathlib v4

Def category_theory.instances.AddCommGroup.forget_to_Group

Modification history

2019-05-31 06:43
src/group_theory/category.lean
chore(category_theory): move all instances (e.g. Top, CommRing, Meas) into the root namespace (#1074) …
Deleted category_theory.instances.AddCommGroup.forget_to_GroupView on Github →
2019-03-28 14:01
src/category_theory/instances/groups.lean
feat(category_theory/instances): category of groups (#749)
Added category_theory.instances.AddCommGroup.forget_to_GroupView on Github →