chore(data/complex/module): split out orientation to a separate file (#…

…18824)

This removes the imports

- linear_algebra.matrix.determinant
- linear_algebra.matrix.mv_polynomial
- linear_algebra.matrix.adjugate
- linear_algebra.matrix.nonsingular_inverse
- linear_algebra.matrix.basis
- linear_algebra.determinant
- linear_algebra.orientation

from `data.complex.module`, which aren't otherwise needed here.



Co-authored-by: Scott Morrison <scott.morrison@gmail.com>

src/analysis/inner_product_space/two_dim.lean

@@ -5,6 +5,7 @@ Authors: Heather Macbeth
 -/
 import analysis.inner_product_space.dual
 import analysis.inner_product_space.orientation
+import data.complex.orientation
 import tactic.linear_combination
 
 /-!

src/data/complex/module.lean

@@ -3,7 +3,6 @@ Copyright (c) 2020 Alexander Bentkamp, Sébastien Gouëzel. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Alexander Bentkamp, Sébastien Gouëzel, Eric Wieser
 -/
-import linear_algebra.orientation
 import algebra.order.smul
 import data.complex.basic
 import data.fin.vec_notation
@@ -167,9 +166,6 @@ by simp [← finrank_eq_rank, finrank_real_complex, bit0]
 circle. -/
 lemma finrank_real_complex_fact : fact (finrank ℝ ℂ = 2) := ⟨finrank_real_complex⟩
 
-/-- The standard orientation on `ℂ`. -/
-protected noncomputable def orientation : orientation ℝ ℂ (fin 2) := complex.basis_one_I.orientation
-
 end complex
 
 /- Register as an instance (with low priority) the fact that a complex vector space is also a real

src/data/complex/orientation.lean

@@ -0,0 +1,21 @@
+/-
+Copyright (c) 2021 Heather Macbeth. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Heather Macbeth
+-/
+import data.complex.module
+import linear_algebra.orientation
+
+/-!
+# The standard orientation on `ℂ`.
+
+This had previously been in `linear_algebra.orientation`,
+but keeping it separate results in a significant import reduction.
+-/
+
+namespace complex
+
+/-- The standard orientation on `ℂ`. -/
+protected noncomputable def orientation : orientation ℝ ℂ (fin 2) := complex.basis_one_I.orientation
+
+end complex