polarBilin_toQuadraticMap — Mathlib

English

The bilinear form obtained from the polar of a quadratic map is twice the original quadratic map.

Русский

Билинейная форма, получаемая из полярной квадратичной карты, равна удвоенной исходной квадратичной карте.

LaTeX

$$$\operatorname{polarBilin} (toQuadraticMap B) = B + \text{flip} B$$$

Lean4

theorem polarBilin_toQuadraticMap : polarBilin (toQuadraticMap B) = B + flip B :=
  LinearMap.ext₂ polar_toQuadraticMap

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