ofMatrix — Mathlib

English

A positive definite matrix M on n×n(𝕜) induces an inner product on the space (n → 𝕜) by ⟪x, y⟫ = xᴴ M y, making it into an inner product space with respect to this product.

Русский

Положительно определённая матрица M на M×M порождает скалярное произведение ⟪x, y⟫ = xᴴ M y на пространстве 𝕜^n, превращая его в пространство с этим скалярным произведением.

LaTeX

$$$\langle x,y\rangle = x^* M y \, (x,y\in \mathbb{K}^n)$.$$

Lean4

/-- A positive definite matrix `M` induces an inner product `⟪x, y⟫ = xᴴMy`. -/
def ofMatrix {M : Matrix n n 𝕜} (hM : M.PosDef) :
    @InnerProductSpace 𝕜 (n → 𝕜) _ (NormedAddCommGroup.ofMatrix hM).toSeminormedAddCommGroup :=
  InnerProductSpace.ofCore _

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