feat: port LinearAlgebra.AffineSpace.Independent (#3341)

Co-authored-by: Moritz Firsching <firsching@google.com> Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
leanprover-community · Apr 21, 2023 · 94d947d · 94d947d
1 parent 408fbe2
commit 94d947d
Show file tree

Hide file tree

Showing 2 changed files with 987 additions and 0 deletions.
diff --git a/Mathlib.lean b/Mathlib.lean
@@ -1335,6 +1335,7 @@ import Mathlib.LinearAlgebra.AffineSpace.AffineMap
 import Mathlib.LinearAlgebra.AffineSpace.AffineSubspace
 import Mathlib.LinearAlgebra.AffineSpace.Basic
 import Mathlib.LinearAlgebra.AffineSpace.Combination
+import Mathlib.LinearAlgebra.AffineSpace.Independent
 import Mathlib.LinearAlgebra.AffineSpace.Midpoint
 import Mathlib.LinearAlgebra.AffineSpace.MidpointZero
 import Mathlib.LinearAlgebra.AffineSpace.Ordered