feat: port LinearAlgebra.SesquilinearForm (#2607)

Co-authored-by: Moritz Firsching <firsching@google.com> Co-authored-by: Jireh Loreaux <loreaujy@gmail.com>
leanprover-community · Mar 22, 2023 · accbdce · accbdce
1 parent 1bd5066
commit accbdce
Show file tree

Hide file tree

Showing 2 changed files with 892 additions and 0 deletions.
diff --git a/Mathlib.lean b/Mathlib.lean
@@ -1122,6 +1122,7 @@ import Mathlib.LinearAlgebra.Projection
 import Mathlib.LinearAlgebra.Quotient
 import Mathlib.LinearAlgebra.Ray
 import Mathlib.LinearAlgebra.SModEq
+import Mathlib.LinearAlgebra.SesquilinearForm
 import Mathlib.LinearAlgebra.Span
 import Mathlib.LinearAlgebra.TensorProduct
 import Mathlib.Logic.Basic