Mathlib v3 is deprecated. Go to Mathlib v4

Def category_theory.limits.mono_factorisation.of_arrow_iso

Modification history

2021-10-29 14:39

src/category_theory/limits/shapes/images.lean

feat(category_theory/limits/shapes/images): some explicit instances of has_image_map (#9977)

Added category_theory.limits.mono_factorisation.of_arrow_iso View on Github →