toQuadraticForm — Mathlib

English

The quadratic map associated to the bilinear form dualProd equals 2 times the dualProd quadratic form, i.e., the bilinearization of the dual pairing yields twice the original form.

Русский

Квадратичное отображение, связанное с билинейной формой dualProd, равно 2 раз dualProd; билинеаризация пары даёт двойную форму.

LaTeX

$$$ (LinearMap.dualProd R M).toQuadraticMap = 2 \\cdot dualProd R M $$$

Lean4

@[simp]
theorem _root_.LinearMap.dualProd.toQuadraticForm : (LinearMap.dualProd R M).toQuadraticMap = 2 • dualProd R M :=
  ext fun _a => (two_nsmul _).symm

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