Commit 2025-03-17 09:28 54999515

View on Github →

feat: Matrix.kroneckerTMul as an AlgEquiv (#21148) Or phrased alternatively, this provides more results about tensor products of matrices. Zulip threads

Estimated changes

Modified Mathlib/Data/Matrix/Composition.lean

Modified Mathlib/Data/Matrix/Kronecker.lean

deleted theorem Matrix.inv_kronecker

Modified Mathlib/LinearAlgebra/Matrix/NonsingularInverse.lean

added theorem Matrix.inv_kronecker

Modified Mathlib/LinearAlgebra/Pi.lean

added theorem LinearMap.lsum_piSingle

Modified Mathlib/RingTheory/MatrixAlgebra.lean

added def Matrix.kroneckerTMulAlgEquiv

added theorem Matrix.kroneckerTMulAlgEquiv_apply

added theorem Matrix.kroneckerTMulAlgEquiv_symm_apply

added theorem kroneckerTMulAlgEquiv_symm_stdBasisMatrix_tmul

added def kroneckerTMulLinearEquiv

added theorem kroneckerTMulLinearEquiv_mul

added theorem kroneckerTMulLinearEquiv_one

added theorem kroneckerTMulLinearEquiv_tmul

Modified Mathlib/RingTheory/MatrixPolynomialAlgebra.lean