Mathlib v3 is deprecated. Go to Mathlib v4

Theorem reflection_sub

Modification history

2022-11-17 13:13
src/analysis/inner_product_space/projection.lean
refactor(analysis): change the symbol for norm to align with the unicode spec (#17575) …
Modified reflection_subView on Github →
2021-11-21 18:40
src/analysis/inner_product_space/projection.lean
feat(analysis/inner_product_space/projection): orthogonal group is generated by reflections (#10381)
Added reflection_subView on Github →