map_add_add_add_map — Mathlib

English

For all x,y,z ∈ M, the polarization relation holds: Q(x+y+z) + Q(x) + Q(y) + Q(z) = Q(x+y) + Q(y+z) + Q(z+x).

Русский

Для любых x,y,z ∈ M выполняется тождество поляризации: Q(x+y+z) + Q(x) + Q(y) + Q(z) = Q(x+y) + Q(y+z) + Q(z+x).

LaTeX

$$Q(x+y+z) + Q x + Q y + Q z = Q(x+y) + Q(y+z) + Q(z+x)$$

Lean4

theorem map_add_add_add_map (x y z : M) : Q (x + y + z) + (Q x + Q y + Q z) = Q (x + y) + Q (y + z) + Q (z + x) :=
  by
  obtain ⟨B, h⟩ := Q.exists_companion
  rw [add_comm z x]
  simp only [h, LinearMap.map_add₂]
  abel

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