Commit 2020-08-31 22:11 be3b1758

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.)