Mathlib Changelog
v4
Changelog
About
Github
Theorem
Matrix.IsUnit.kronecker
Modification history
2025-10-18 19:47
Mathlib/LinearAlgebra/Matrix/GeneralLinearGroup/Defs.lean
feat(LinearAlgebra/Matrix/PosDef): kronecker of positive (semi-)definite matrices is positive (semi-)definite (#28097) …
Added
Matrix.IsUnit.kronecker
View on Github →