polar_toQuadraticMap — Mathlib

English

For any bilinear map B, the polar form of the quadratic map associated to B is given by the sum B(x,y) + B(y,x).

Русский

Для билинейного отображения B полярная форма квадратичной карты, ассоциированной с B, равна B(x,y) + B(y,x).

LaTeX

$$$\operatorname{polar}(\operatorname{toQuadraticMap} B)\; x\; y = B(x,y) + B(y,x)$$$

Lean4

theorem polar_toQuadraticMap (x y : M) : polar (toQuadraticMap B) x y = B x y + B y x := by
  simp only [polar, toQuadraticMap_apply, map_add, add_apply, add_assoc, add_comm (B y x) _, add_sub_cancel_left,
    sub_eq_add_neg _ (B y y), add_neg_cancel_left]

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