chore(ring_theory/algebra): move instances about complex to get rid o…

…f dependency (#2549) Previously `ring_theory.algebra` imported the complex numbers. This PR moves some instances in order to get rid of that dependency.
leanprover-community · Apr 27, 2020 · fd3afb4 · fd3afb4
1 parent 948d0ff
commit fd3afb4
Show file tree

Hide file tree

Showing 5 changed files with 27 additions and 14 deletions.
diff --git a/src/analysis/convex/basic.lean b/src/analysis/convex/basic.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Alexander Bentkamp, Yury Kudriashov
 -/
 import data.set.intervals
-import ring_theory.algebra
+import data.complex.module
 import algebra.pointwise
 
 /-!

diff --git a/src/data/complex/module.lean b/src/data/complex/module.lean
@@ -0,0 +1,24 @@
+/-
+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
+-/
+import data.complex.basic ring_theory.algebra
+/-!
+This file contains two instance, the fact the ℂ is an ℝ algebra,
+and an instance to view any complex vector space as a
+real vector space
+-/
+noncomputable theory
+
+namespace complex
+
+instance algebra_over_reals : algebra ℝ ℂ := (ring_hom.of coe).to_algebra
+
+end complex
+
+/- Register as an instance (with low priority) the fact that a complex vector space is also a real
+vector space. -/
+instance module.complex_to_real (E : Type*) [add_comm_group E] [module ℂ E] : module ℝ E :=
+module.restrict_scalars ℝ ℂ E
+attribute [instance, priority 900] module.complex_to_real
diff --git a/src/ring_theory/algebra.lean b/src/ring_theory/algebra.lean
@@ -3,7 +3,6 @@ Copyright (c) 2018 Kenny Lau. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Kenny Lau, Yury Kudryashov
 -/
-import data.complex.basic
 import data.matrix.basic
 import linear_algebra.tensor_product
 import algebra.commute
@@ -389,12 +388,6 @@ instance algebra_rat {α} [division_ring α] [char_zero α] : algebra ℚ α :=
 
 end rat
 
-namespace complex
-
-instance algebra_over_reals : algebra ℝ ℂ := (ring_hom.of coe).to_algebra
-
-end complex
-
 /-- A subalgebra is a subring that includes the range of `algebra_map`. -/
 structure subalgebra (R : Type u) (A : Type v)
   [comm_ring R] [ring A] [algebra R A] : Type v :=
@@ -649,10 +642,4 @@ def linear_map.restrict_scalars (f : E →ₗ[S] F) : E →ₗ[R] F :=
 @[simp, norm_cast squash] lemma linear_map.coe_restrict_scalars_eq_coe (f : E →ₗ[S] F) :
   (f.restrict_scalars R : E → F) = f := rfl
 
-/- Register as an instance (with low priority) the fact that a complex vector space is also a real
-vector space. -/
-instance module.complex_to_real (E : Type*) [add_comm_group E] [module ℂ E] : module ℝ E :=
-module.restrict_scalars ℝ ℂ E
-attribute [instance, priority 900] module.complex_to_real
-
 end restrict_scalars
diff --git a/src/ring_theory/power_series.lean b/src/ring_theory/power_series.lean
@@ -5,6 +5,7 @@ Authors: Johan Commelin, Kenny Lau
 -/
 import data.mv_polynomial
 import ring_theory.ideal_operations
+import tactic.linarith
 
 /-!
 # Formal power series

diff --git a/src/topology/algebra/polynomial.lean b/src/topology/algebra/polynomial.lean
@@ -7,6 +7,7 @@ Analytic facts about polynomials.
 -/
 import topology.algebra.ring
 import data.polynomial
+import data.real.cau_seq
 
 open polynomial is_absolute_value