Theorem CategoryTheory.IsCardinalLocallyPresentable.iff_exists_isStrongGenerator

Modification history

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