Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-03-16 14:46 555528e1

View on Github →

feat(category_theory/image): comparison maps for precomposition (#2153)

feat(category_theory/image): comparison maps for precomposition
remove duplicate argument
unused argument

Estimated changes

Modified src/category_theory/limits/shapes/images.lean

added def category_theory.limits.image.eq_to_hom

added def category_theory.limits.image.eq_to_iso

added def category_theory.limits.image.pre_comp

added theorem category_theory.limits.image.pre_comp_comp