intCast — Mathlib

English

Let n be a positive integer and R a ring with a compatible star-order. Then for any integer d > 0, the scalar matrix d I_n is positive definite.

Русский

Пусть n — натуральное число, R — кольцо с совместимым звездно-упорядочением. Тогда для любого целого d > 0 матрица d I_n положительно определена.

LaTeX

$$$$ 0 < d \\implies \\operatorname{PosDef}(d I_n) $$$$

Lean4

protected theorem intCast [StarOrderedRing R] [DecidableEq n] [NoZeroDivisors R] (d : ℤ) (hd : 0 < d) :
    PosDef (d : Matrix n n R) :=
  ⟨isHermitian_intCast _, fun x hx =>
    by
    rw [intCast_mulVec, Int.cast_smul_eq_zsmul, dotProduct_smul]
    exact zsmul_pos (dotProduct_star_self_pos_iff.mpr hx) hd⟩

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