Mathlib v3 is deprecated. Go to Mathlib v4

Theorem category_theory.limits.mono_factorisation.kernel_ι_comp

Modification history

2022-03-29 18:32

src/category_theory/limits/shapes/kernels.lean

feat(category_theory/abelian): constructor in terms of coimage-image comparison (#12972) …

Added category_theory.limits.mono_factorisation.kernel_ι_comp View on Github →