mathlib3

be3b1758 - feat(analysis/normed_space/real_inner_product): inner_add_sub_eq_zero_iff (#4004)

feat(analysis/normed_space/real_inner_product): inner_add_sub_eq_zero_iff (#4004) Add a lemma that the sum and difference of two vectors are orthogonal if and only if they have the same norm. (This can be interpreted geometrically as saying e.g. that a median of a triangle from a vertex is orthogonal to the opposite edge if and only if the triangle is isosceles at that vertex.)