Theorems · Theorem · functional analysis

inner_map_self_eq_zero

∀ {V : Type u_4} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℂ V] (T : V →ₗ[ℂ] V),
  (∀ (x : V), inner ℂ (T x) x = 0) ↔ T = 0

A linear map T is zero, if and only if the identity ⟪T x, x⟫_ℂ = 0 holds for all x.

Defined in

Mathlib.Analysis.InnerProductSpace.LinearMap

Cited by

1 results in Mathlib

Foundations

Depth 170 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

NormedAddCommGroupInnerProductSpace