smul — Mathlib

English

If x is positive definite and a>0 then a • x is positive definite.

Русский

Если x положительно определена и a>0, то a·x положительно определена.

LaTeX

$$$$ \\operatorname{PosDef}(x) \\to a > 0 \\to \\operatorname{PosDef}(a \\cdot x). $$$$

Lean4

protected theorem smul {α : Type*} [CommSemiring α] [PartialOrder α] [StarRing α] [StarOrderedRing α] [Algebra α R]
    [StarModule α R] [PosSMulStrictMono α R] {x : Matrix n n R} (hx : x.PosDef) {a : α} (ha : 0 < a) : (a • x).PosDef :=
  by
  refine ⟨IsSelfAdjoint.smul (IsSelfAdjoint.of_nonneg ha.le) hx.1, fun y hy => ?_⟩
  simp only [smul_mulVec, dotProduct_smul]
  exact smul_pos ha (hx.2 _ hy)

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