Skip to content

Commit 24248ce

Browse files
chore(Mathlib/LinearAlgebra/Matrix/Kronecker.lean): automated extraction (leanprover-community#36136)
This PR was automatically created from PR leanprover-community#35233 by @kim-em via a [review comment](leanprover-community#35233 (comment)) by @Vierkantor. Co-authored-by: kim-em <477956+kim-em@users.noreply.github.com>
1 parent a48343c commit 24248ce

File tree

1 file changed

+0
-1
lines changed

1 file changed

+0
-1
lines changed

Mathlib/LinearAlgebra/Matrix/Kronecker.lean

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -5,7 +5,6 @@ Authors: Filippo A. E. Nuccio, Eric Wieser
55
-/
66
module
77

8-
public import Mathlib.GroupTheory.GroupAction.Ring
98
public import Mathlib.LinearAlgebra.Matrix.Determinant.Basic
109
public import Mathlib.LinearAlgebra.Matrix.Trace
1110
public import Mathlib.RingTheory.TensorProduct.Basic

0 commit comments

Comments
 (0)