Theorems · Theorem · linear algebra

Matrix.PosDef.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.PosDef → y.PosDef → (Matrix.kroneckerMap (fun x1 x2 => x1 * x2) x y).PosDef

The kronecker of two positive definite matrices is positive definite.

Defined in

Mathlib.Analysis.Matrix.Order

Cited by

1 results in Mathlib

Foundations

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

Assumes

RCLikeFiniteFinite