Theorems · Theorem · linear algebra

LinearMap.BilinForm.IsSymm.polarization

∀ {M : Type u_2} [inst : AddCommMonoid M] {R : Type u_8} [inst_1 : Field R] [NeZero 2] [inst_3 : Module R M]
  {B : LinearMap.BilinForm R M} (x y : M), B.IsSymm → (B x) y = ((B (x + y)) (x + y) - (B x) x - (B y) y) / 2

Polarization identity: a symmetric bilinear form can be expressed through the values it takes on the diagonal.

Defined in

Mathlib.LinearAlgebra.BilinearForm.Properties

Cited by

1 results in Mathlib

Foundations

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

Assumes

AddCommMonoidFieldNeZeroModule