Theorem CategoryTheory.IsStrongGenerator.colimitsCardinalClosure_eq_isCardinalPresentable

Modification history

2025-12-05 16:31
Mathlib/CategoryTheory/Presentable/StrongGenerator.lean
feat(CategoryTheory): locally presentable categories and strong generators (#30241) …
Added CategoryTheory.IsStrongGenerator.colimitsCardinalClosure_eq_isCardinalPresentableView on Github →