inner_map_self_eq_zero

Stream: mathlib4

[Iván Renison]

Hi, in Analysis.InnerProductSpace.LinearMap we have this two theorems:

theorem inner_map_self_eq_zero (T : V →ₗ[ℂ] V) : (∀ x : V, ⟪T x, x⟫_ℂ = 0) ↔ T = 0
theorem ext_inner_map (S T : V →ₗ[ℂ] V) : (∀ x : V, ⟪S x, x⟫_ℂ = ⟪T x, x⟫_ℂ) ↔ S = T

I wanted to ask, do you know if there a reason they are for ℂ instead of for 𝕜 (with RCLike 𝕜)?

[Sébastien Gouëzel]

A rotation by $\pi/2$ in the plane sends every vector to an orthogonal vector, and yet it is non zero...

[Iván Renison]

Ah, okay, yes, thanks

[Jireh Loreaux]

Note, however, that it works for symmetric operators: docs#LinearMap.IsSymmetric.inner_map_self_eq_zero

[Iván Renison]

Great! Thanks

[Iván Renison]

And do you know if we have this versions?

lemma LinearMap.re_inner_eq_zero (T : E →ₗ[𝕜] E) :
    (∀x y : E, RCLike.re ⟪T x, y⟫ = 0) ↔ T = 0 := sorry

lemma LinearMap.inner_eq_zero (T : E →ₗ[𝕜] E) :
    (∀x y : E, ⟪T x, y⟫ = 0) ↔ T = 0 := sorry

[Iván Renison]

Also, in docs#LinearMap.IsSymmetric.inner_map_self_eq_zero I see that the description says if and only if `⟪T x, x⟫_ℝ = 0` , but the theorem uses inner 𝕜, is that an error?
I think both versions of the theorem are valid