inner product space eq

Stream: Is there code for X?

[Moritz Doll]

Is this lemma in mathlib? I haven't found it, but I feel like it should exist

import analysis.inner_product_space.basic

variables (𝕜 : Type*) {E : Type*}
variables [is_R_or_C 𝕜] [inner_product_space 𝕜 E]

example {x x' : E} (h : ∀ y : E,  inner x y =  (inner x' y : 𝕜)) : x = x' :=
begin
  specialize h (x - x'),
  rw [←sub_eq_zero, ←inner_self_eq_zero, inner_sub_left, sub_eq_zero],
  exact h,
end

[Eric Wieser]

Maybe it's named something like docs#inner_left_inj?

[Frédéric Dupuis]

docs#inner_product_space.ext_inner_right

[Eric Wieser]

I guess we don't have the version that says function.injective (inner x)?

[Wrenna Robson]

Isn't that docs#inner_product_space.ext_inner_left?

[Wrenna Robson]

I guess maybe that puts the quantifier in a different place.