Theorem CategoryTheory.OrthogonalReflection.D₂.condition

Modification history

2025-11-08 14:58

Mathlib/CategoryTheory/Presentable/OrthogonalReflection.lean

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

Added CategoryTheory.OrthogonalReflection.D₂.condition View on Github →