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⟩