Theorem CategoryTheory.OrthogonalReflection.isRightAdjoint_ι

Modification history

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