Commit 2025-10-18 19:47 41e1a248

feat(LinearAlgebra/Matrix/PosDef): kronecker of positive (semi-)definite matrices is positive (semi-)definite (#28097) This first shows that U * x * star U is positive (semi-)definite if and only if x is, for an invertible matrix U in a not necessarily commutative star-ring. Then using the spectral theorem, it follows that the kronecker of positive (semi-)definite matrices is positive (semi-)definite.