Theorems · Theorem · linear algebra

Matrix.PosSemidef.kronecker

∀ {𝕜 : Type u_1} {n : Type u_2} [inst : RCLike 𝕜] [Finite n] {m : Type u_3} [Finite m] {x : Matrix n n 𝕜}
  {y : Matrix m m 𝕜}, x.PosSemidef → y.PosSemidef → (Matrix.kroneckerMap (fun x1 x2 => x1 * x2) x y).PosSemidef

The kronecker product of two positive semi-definite matrices is positive semi-definite.

Defined in

Mathlib.Analysis.Matrix.Order

Cited by

2 results in Mathlib

Foundations

Depth 266 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

RCLikeFiniteFinite