smul — Mathlib

English

Positive definiteness is preserved under multiplication by a positive scalar.

Русский

Положительная определенность сохраняется при умножении на положительное скалярное число.

LaTeX

$$$\\mathrm{PosDef}(a\\cdot Q) \\,\\text{whenever } a>0$, given suitable positivity conditions on the scalar and module.$$

Lean4

theorem smul {R} [CommSemiring R] [PartialOrder R] [Module R M] [Module R N] [PosSMulStrictMono R N]
    {Q : QuadraticMap R M N} (h : PosDef Q) {a : R} (a_pos : 0 < a) : PosDef (a • Q) := fun x hx =>
  smul_pos a_pos (h x hx)

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