inner_map_self_eq_zero — Mathlib

English

For a complex-linear map T, the statement that ⟪T x, x⟫ = 0 for all x implies T = 0.

Русский

Если для комплексного линейного отображения T скалярное произведение ⟪T x, x⟫ равно нулю для всех x, то T=0.

LaTeX

$$$ (\forall x, \langle T x, x \rangle_\mathbb{C} = 0) \ \iff \ T=0. $$$

Lean4

/-- A linear map `T` is zero, if and only if the identity `⟪T x, x⟫_ℂ = 0` holds for all `x`.
-/
theorem inner_map_self_eq_zero (T : V →ₗ[ℂ] V) : (∀ x : V, ⟪T x, x⟫_ℂ = 0) ↔ T = 0 :=
  by
  constructor
  · intro hT
    ext x
    rw [LinearMap.zero_apply, ← @inner_self_eq_zero ℂ V, inner_map_polarization]
    simp only [hT]
    simp
  · rintro rfl x
    simp only [LinearMap.zero_apply, inner_zero_left]

Похожие утверждения