English
Simp lemma: nat cast yields positive endomorphisms.
Русский
Лемма-упрощение: приведённое к целым числам отображение даёт положительные эндоморфизмы.
LaTeX
$$$$\text{IsPositive}(\mathrm{natCast}(n))$$$$
Lean4
/-- `A.toEuclideanLin` is positive if and only if `A` is positive semi-definite. -/
@[simp]
theorem _root_.Matrix.isPositive_toEuclideanLin_iff {n : Type*} [Fintype n] [DecidableEq n] {A : Matrix n n 𝕜} :
A.toEuclideanLin.IsPositive ↔ A.PosSemidef :=
by
simp_rw [LinearMap.IsPositive, ← Matrix.isHermitian_iff_isSymmetric, inner_re_symm,
EuclideanSpace.inner_eq_star_dotProduct, Matrix.piLp_ofLp_toEuclideanLin, Matrix.toLin'_apply,
dotProduct_comm (A.mulVec _), Matrix.PosSemidef, and_congr_right_iff, RCLike.nonneg_iff (K := 𝕜)]
refine fun hA ↦ (EuclideanSpace.equiv n 𝕜).forall_congr' fun x ↦ ?_
simp [hA.im_star_dotProduct_mulVec_self]
