Theorem CategoryTheory.SmallObject.llp_rlp_ιObj

Modification history

2025-02-15 18:13

Mathlib/CategoryTheory/SmallObject/IsCardinalForSmallObjectArgument.lean

feat(CategoryTheory/SmallObject): the functorial factorization (#21911) …

Added CategoryTheory.SmallObject.llp_rlp_ιObj View on Github →