Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-11-21 18:40 2168297e

View on Github →

feat(analysis/inner_product_space/projection): orthogonal group is generated by reflections (#10381)

Estimated changes

Modified docs/undergrad.yaml

Modified src/analysis/inner_product_space/basic.lean

added theorem mem_orthogonal_singleton_of_inner_left

added theorem mem_orthogonal_singleton_of_inner_right

Modified src/analysis/inner_product_space/projection.lean

added theorem linear_isometry_equiv.reflections_generate

added theorem linear_isometry_equiv.reflections_generate_dim

added theorem linear_isometry_equiv.reflections_generate_dim_aux

added theorem reflection_sub

added theorem reflection_trans_reflection

modified theorem submodule.finrank_add_finrank_orthogonal