Theorem CategoryTheory.MorphismProperty.exists_hom_of_isFinitelyPresentable

Modification history

2025-09-18 18:51
Mathlib/CategoryTheory/MorphismProperty/Ind.lean
feat(CategoryTheory/MorphismProperty): define `ind P` (#29380) …
Added CategoryTheory.MorphismProperty.exists_hom_of_isFinitelyPresentableView on Github →