Theorem CategoryTheory.OrthogonalReflection.isLocal_isLocal_reflection

Modification history

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