Commit 2023-05-26 23:07 78c6eda1

View on Github →

feat: port Algebra.Category.GroupCat.Images (#4403)

Estimated changes

Modified Mathlib.lean

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

added def AddCommGroupCat.factorThruImage

added theorem AddCommGroupCat.image.fac

added theorem AddCommGroupCat.image.lift_fac

added def AddCommGroupCat.image.ι

added def AddCommGroupCat.image

added def AddCommGroupCat.monoFactorisation