2025-01-20 16:09
Mathlib/CategoryTheory/Localization/LocallySmall.lean
feat(CategoryTheory/Localization): HasLocalization holds iff the localized category is locally small (#20670) …
Added CategoryTheory.MorphismProperty.locallySmall_of_hasLocalization