Def CategoryTheory.OrthogonalReflection.D₂

Modification history

2025-11-08 14:58

Mathlib/CategoryTheory/Presentable/OrthogonalReflection.lean

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

Added CategoryTheory.OrthogonalReflection.D₂ View on Github →