Def CategoryTheory.OrthogonalReflection.D₁.obj₂

Modification history

2025-11-08 14:58

Mathlib/CategoryTheory/Presentable/OrthogonalReflection.lean

feat(CategoryTheory): the orthogonal-reflection construction (#30492) …

Added CategoryTheory.OrthogonalReflection.D₁.obj₂ View on Github →