Mathlib v3 is deprecated. Go to Mathlib v4

Theorem linear_isometry_equiv.reflections_generate_dim_aux

Modification history

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 linear_isometry_equiv.reflections_generate_dim_auxView on Github →