inner_map_self_eq_zero — Mathlib

English

A symmetric linear map T is zero if and only if ⟪T x, x⟫ = 0 for all x.

Русский

Симметричное линейное отображение T нуль-отображение тогда и только тогда, когда ⟪T x, x⟫ = 0 для всех x.

LaTeX

$$$(∀ x, ⟪T x, x⟫ = 0) \iff T = 0$ for symmetric T$$

Lean4

/-- A symmetric linear map `T` is zero if and only if `⟪T x, x⟫_ℝ = 0` for all `x`.
See `inner_map_self_eq_zero` for the complex version without the symmetric assumption. -/
theorem inner_map_self_eq_zero {T : E →ₗ[𝕜] E} (hT : T.IsSymmetric) : (∀ x, ⟪T x, x⟫ = 0) ↔ T = 0 :=
  by
  simp_rw [LinearMap.ext_iff, zero_apply]
  refine ⟨fun h x => ?_, fun h => by simp_rw [h, inner_zero_left, forall_const]⟩
  rw [← @inner_self_eq_zero 𝕜, hT.inner_map_polarization]
  simp_rw [h _]
  ring

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