Theorems · Theorem · functional analysis

inner_map_polarization

∀ {V : Type u_4} [inst : SeminormedAddCommGroup V] [inst_1 : InnerProductSpace ℂ V] (T : V →ₗ[ℂ] V) (x y : V),
  inner ℂ (T y) x =
    (inner ℂ (T (x + y)) (x + y) - inner ℂ (T (x - y)) (x - y) +
          Complex.I * inner ℂ (T (x + Complex.I • y)) (x + Complex.I • y) -
        Complex.I * inner ℂ (T (x - Complex.I • y)) (x - Complex.I • y)) /
      4

A complex polarization identity, with a linear map.

Defined in

Mathlib.Analysis.InnerProductSpace.LinearMap

Cited by

2 results in Mathlib

Foundations

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

Assumes

SeminormedAddCommGroupInnerProductSpace