feat: port LinearAlgebra.Matrix.SesquilinearForm (#4315)

Dot notation is broken here, but I don't think there is anything we can do about it.
leanprover-community · May 25, 2023 · e7890e2 · e7890e2
1 parent 24e633e
commit e7890e2
Show file tree

Hide file tree

Showing 2 changed files with 766 additions and 0 deletions.
diff --git a/Mathlib.lean b/Mathlib.lean
@@ -1670,6 +1670,7 @@ import Mathlib.LinearAlgebra.Matrix.NonsingularInverse
 import Mathlib.LinearAlgebra.Matrix.Orthogonal
 import Mathlib.LinearAlgebra.Matrix.Polynomial
 import Mathlib.LinearAlgebra.Matrix.Reindex
+import Mathlib.LinearAlgebra.Matrix.SesquilinearForm
 import Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup
 import Mathlib.LinearAlgebra.Matrix.Symmetric
 import Mathlib.LinearAlgebra.Matrix.ToLin