Commit 2023-05-26 09:02 4e6f5745

View on Github →

feat: port Algebra.Category.Module.Images (#4385)

Estimated changes

Modified Mathlib.lean

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

added def ModuleCat.factorThruImage

added theorem ModuleCat.image.fac

added theorem ModuleCat.image.lift_fac

added def ModuleCat.image.ι

added def ModuleCat.image

added theorem ModuleCat.imageIsoRange_hom_subtype

added theorem ModuleCat.imageIsoRange_inv_image_ι

added def ModuleCat.monoFactorisation