Def CategoryTheory.OrthogonalReflection.D₂.multispanShape

Modification history

2025-11-08 14:58

Mathlib/CategoryTheory/Presentable/OrthogonalReflection.lean

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

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