feat port: LinearAlgebra.Orientation (#3777)

I had to add a bunch of `set_option synthInstance.etaExperiment true`, `set_option maxHeartbeats` and `set_option synthInstance.maxHeartbeats` to this file I tried to use the methods described in this [Zulip thread](https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/maxHeartbeats/near/356217898) to remove some of the `maxHeartbeats` but I was not successful. Co-authored-by: Scott Morrison <scott.morrison@anu.edu.au>
leanprover-community · May 8, 2023 · 39a4242 · 39a4242
1 parent 3c74294
commit 39a4242
Show file tree

Hide file tree

Showing 2 changed files with 446 additions and 0 deletions.
diff --git a/Mathlib.lean b/Mathlib.lean
@@ -1479,6 +1479,7 @@ import Mathlib.LinearAlgebra.Matrix.ZPow
 import Mathlib.LinearAlgebra.Multilinear.Basic
 import Mathlib.LinearAlgebra.Multilinear.Basis
 import Mathlib.LinearAlgebra.Multilinear.TensorProduct
+import Mathlib.LinearAlgebra.Orientation
 import Mathlib.LinearAlgebra.Pi
 import Mathlib.LinearAlgebra.Prod
 import Mathlib.LinearAlgebra.Projection