Theorem kroneckerTMulLinearEquiv_one

Modification history

2025-06-12 04:59

Mathlib/RingTheory/MatrixAlgebra.lean

refactor: make `Matrix.kroneckerTMulAlgEquiv` heterogeneous (#25693) …

Modified kroneckerTMulLinearEquiv_one View on Github →

2025-03-17 09:28

Mathlib/RingTheory/MatrixAlgebra.lean

feat: `Matrix.kroneckerTMul` as an `AlgEquiv` (#21148) …

Added kroneckerTMulLinearEquiv_one View on Github →