English
Let S,T be complex-linear endomorphisms on a vector space V. Then S = T if and only if for every x in V, ⟪Sx, x⟫ = ⟪Tx, x⟫.
Русский
Пусть S,T — комплексно-линейные отображения V → V. Тогда S = T тогда и только тогда, когда для каждого x ∈ V выполняется ⟪Sx, x⟫ = ⟪Tx, x⟫.
LaTeX
$$$ ( \\forall x \\, : \\, V, \\ \\langle S x, x \\rangle_{\\mathbb{C}} = \\langle T x, x \\rangle_{\\mathbb{C}} ) \\iff S = T $$$
Lean4
/-- Two linear maps `S` and `T` are equal, if and only if the identity `⟪S x, x⟫_ℂ = ⟪T x, x⟫_ℂ` holds
for all `x`.
-/
theorem ext_inner_map (S T : V →ₗ[ℂ] V) : (∀ x : V, ⟪S x, x⟫_ℂ = ⟪T x, x⟫_ℂ) ↔ S = T :=
by
rw [← sub_eq_zero, ← inner_map_self_eq_zero]
refine forall_congr' fun x => ?_
rw [LinearMap.sub_apply, inner_sub_left, sub_eq_zero]
