Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-11-12 02:18 f435f954

View on Github →

feat(analysis/inner_product_space): ext lemmas for dense subspaces (#17450)

Estimated changes

Modified src/analysis/inner_product_space/basic.lean

added theorem submodule.sub_mem_orthogonal_of_inner_left

added theorem submodule.sub_mem_orthogonal_of_inner_right

Modified src/analysis/inner_product_space/projection.lean

added theorem dense.eq_of_inner_left

added theorem dense.eq_of_inner_right

added theorem dense.eq_of_sub_mem_orthogonal

added theorem dense.eq_zero_of_inner_left

added theorem dense.eq_zero_of_inner_right

added theorem dense.eq_zero_of_mem_orthogonal