Mathlib v3 is deprecated. Go to Mathlib v4

Theorem mem_orthogonal_singleton_of_inner_right

Modification history

2022-12-07 12:47

src/analysis/inner_product_space/basic.lean

feat(analysis/inner_product_space): promote implications to iffs (#17727)

Deleted mem_orthogonal_singleton_of_inner_right View on Github →

2021-11-21 18:40

src/analysis/inner_product_space/basic.lean

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

Added mem_orthogonal_singleton_of_inner_right View on Github →