Theorem CategoryTheory.OrthogonalReflection.isLocal_reflectionObj

Modification history

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