smul — Mathlib

English

A nonnegative scalar multiple of a positive semidefinite bilinear form is again positive semidefinite.

Русский

Неотрицательное скалярное умножение положительно полуопределенной билинейной формы снова дает неотрицательно определенную форму.

LaTeX

$$$ B.IsPosSemidef \\to 0 \\le c \\Rightarrow (c \\cdot B).IsPosSemidef $$$

Lean4

protected theorem smul [Preorder R] [PosMulMono R] {B : BilinForm R M} {c : R} (hB : B.IsPosSemidef) (hc : 0 ≤ c) :
    (c • B).IsPosSemidef :=
  isPosSemidef_def.2 ⟨hB.isSymm.smul c, hB.isNonneg.smul hc⟩

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