Theorem CategoryTheory.Limits.Concrete.exists_hom_ι_eq_of_isColimit

Modification history

2026-05-28 22:31
Mathlib/CategoryTheory/Limits/ConcreteCategory/Basic.lean
feat(Algebra/Category): filtered colimits in `AlgCat` (#39145) …
Added CategoryTheory.Limits.Concrete.exists_hom_ι_eq_of_isColimitView on Github →