Commit 2023-05-13 08:38 96a5adb8

View on Github →

feat: port Algebra.Category.Group.Injective (#3908)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Algebra/Category/GroupCat/Injective.lean

added theorem AddCommGroupCat.injective_as_module_of_injective_as_Ab

added theorem AddCommGroupCat.injective_of_injective_as_module