toQuadraticMap' — Mathlib

English

The matrix associated to a quadratic map represents its quadratic form in coordinates.

Русский

Матрица, связанная с квадратичной картой, представляет её квадратичную форму в координатах.

LaTeX

$$toMatrix'(Q) ∈ M_{n×n}(R) represents the quadratic form Q in the standard basis.$$

Lean4

/-- `M.toQuadraticMap'` is the map `fun x ↦ row x * M * col x` as a quadratic form. -/
def toQuadraticMap' (M : Matrix n n R) : QuadraticMap R (n → R) R :=
  LinearMap.BilinMap.toQuadraticMap (Matrix.toLinearMap₂' R M)

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