toQuadraticMap_polarBilin — Mathlib

English

Twice the polar bilinear form of Q equals the quadratic map Q.polarBilin.

Русский

Удвоенная полярная билинейная карта Q равна квадратичной карте Q.polarBilin.

LaTeX

$$$ toQuadraticMap (polarBilin Q) = 2 \cdot Q $$$

Lean4

@[simp]
theorem _root_.QuadraticMap.toQuadraticMap_polarBilin (Q : QuadraticMap R M N) :
    toQuadraticMap (polarBilin Q) = 2 • Q :=
  QuadraticMap.ext fun x => (polar_self _ x).trans <| by simp

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