feat: port LinearAlgebra.Matrix.Transvection (#3700)

Co-authored-by: Moritz Firsching <[email protected]> Co-authored-by: ChrisHughes24 <[email protected]>
leanprover-community · May 10, 2023 · 601c820 · 601c820
1 parent 3d57648
commit 601c820
Show file tree

Hide file tree

Showing 2 changed files with 758 additions and 0 deletions.
diff --git a/Mathlib.lean b/Mathlib.lean
@@ -1441,6 +1441,7 @@ import Mathlib.LinearAlgebra.Matrix.Reindex
 import Mathlib.LinearAlgebra.Matrix.Symmetric
 import Mathlib.LinearAlgebra.Matrix.ToLin
 import Mathlib.LinearAlgebra.Matrix.Trace
+import Mathlib.LinearAlgebra.Matrix.Transvection
 import Mathlib.LinearAlgebra.Matrix.ZPow
 import Mathlib.LinearAlgebra.Multilinear.Basic
 import Mathlib.LinearAlgebra.Multilinear.Basis