Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-03-19 10:59 a20f378f

View on Github →

chore(category_theory/images): fix some minor problems (#2182)

chore(category_theory/images): fix some minor problems
minor
oops, misplaced comment

Estimated changes

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

added theorem category_theory.limits.as_factor_thru_image

deleted theorem category_theory.limits.image.as_c

deleted def category_theory.limits.image.c

deleted theorem category_theory.limits.image.c_ι