feat: port LinearAlgebra.BilinearMap (#2434)

Co-authored-by: casavaca <96765450+casavaca@users.noreply.github.com>
leanprover-community · Feb 28, 2023 · 6ec7f93 · 6ec7f93
1 parent 917b708
commit 6ec7f93
Show file tree

Hide file tree

Showing 2 changed files with 432 additions and 0 deletions.
diff --git a/Mathlib.lean b/Mathlib.lean
@@ -872,6 +872,7 @@ import Mathlib.Lean.Meta
 import Mathlib.Lean.Meta.Simp
 import Mathlib.LinearAlgebra.AffineSpace.Basic
 import Mathlib.LinearAlgebra.Basic
+import Mathlib.LinearAlgebra.BilinearMap
 import Mathlib.LinearAlgebra.Finsupp
 import Mathlib.LinearAlgebra.GeneralLinearGroup
 import Mathlib.LinearAlgebra.LinearIndependent