feat: port Data.Matrix.Kronecker (#4068)

leanprover-community · May 18, 2023 · 968d650 · 968d650
1 parent af2d493
commit 968d650
Show file tree

Hide file tree

Showing 2 changed files with 580 additions and 0 deletions.
diff --git a/Mathlib.lean b/Mathlib.lean
@@ -1053,6 +1053,7 @@ import Mathlib.Data.Matrix.CharP
 import Mathlib.Data.Matrix.DMatrix
 import Mathlib.Data.Matrix.DualNumber
 import Mathlib.Data.Matrix.Hadamard
+import Mathlib.Data.Matrix.Kronecker
 import Mathlib.Data.Matrix.Notation
 import Mathlib.Data.Matrix.PEquiv
 import Mathlib.Data.Matrix.Rank