∀ {𝕜 : 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