Theorem CategoryTheory.MorphismProperty.isRightAdjoint_ι_isLocal

Modification history

2025-12-01 18:53
Mathlib/CategoryTheory/Presentable/OrthogonalReflection.lean
feat(CategoryTheory): localization of locally presentable categories (#30554) …
Added CategoryTheory.MorphismProperty.isRightAdjoint_ι_isLocalView on Github →