polarization — Mathlib

English

A symmetric bilinear form can be expressed via the diagonal values.

Русский

Симметричная билинейная форма может быть выражена через диагональные значения.

LaTeX

$$B.IsSymm → ∀ x y, B x y = (B (x + y) (x + y) - B x x - B y y) / 2$$

Lean4

/-- Polarization identity: a symmetric bilinear form can be expressed through the values
it takes on the diagonal. -/
theorem polarization (x y : M) (hB : B.IsSymm) : B x y = (B (x + y) (x + y) - B x x - B y y) / 2 :=
  by
  simp only [map_add, LinearMap.add_apply]
  rw [hB.eq y x]
  ring_nf
  rw [mul_assoc, inv_mul_cancel₀ two_ne_zero, mul_one]

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