feat: port LinearAlgebra.Projection (#2431)

leanprover-community · Feb 22, 2023 · bd68785 · bd68785
1 parent ae05b30
commit bd68785
Show file tree

Hide file tree

Showing 2 changed files with 469 additions and 0 deletions.
diff --git a/Mathlib.lean b/Mathlib.lean
@@ -842,6 +842,7 @@ import Mathlib.LinearAlgebra.Finsupp
 import Mathlib.LinearAlgebra.GeneralLinearGroup
 import Mathlib.LinearAlgebra.Pi
 import Mathlib.LinearAlgebra.Prod
+import Mathlib.LinearAlgebra.Projection
 import Mathlib.LinearAlgebra.Quotient
 import Mathlib.LinearAlgebra.Span
 import Mathlib.Logic.Basic