Commit 2025-06-12 04:59 5f853838
View on Github →refactor: make Matrix.kroneckerTMulAlgEquiv heterogeneous (#25693)
This generalizes as
-Matrix m m A ⊗[R] Matrix n n B ≃ₐ[R] Matrix (m × n) (m × n) (A ⊗[R] B)
+Matrix m m A ⊗[R] Matrix n n B ≃ₐ[S] Matrix (m × n) (m × n) (A ⊗[R] B)
where R / S / A is a tower of algebras. Notably, when A is commutative this allows S := A.
The module version is similarly generalized.