refactor(topology/algebra/module/basic): don't import determinant (#1…

…7517)

More files on the longest import chain in mathlib.



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

src/analysis/normed/field/basic.lean

@@ -3,6 +3,7 @@ Copyright (c) 2018 Patrick Massot. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Patrick Massot, Johannes Hölzl
 -/
+import algebra.algebra.subalgebra.basic
 import analysis.normed.group.infinite_sum
 import topology.algebra.module.basic
 import topology.instances.ennreal
@@ -1013,3 +1014,6 @@ instance to_normed_comm_ring [normed_comm_ring R] [subring_class S R] (s : S) :
 { mul_comm := mul_comm, .. subring_class.to_normed_ring s }
 
 end subring_class
+
+-- Guard again import creep.
+assert_not_exists restrict_scalars

src/analysis/normed_space/basic.lean

@@ -3,6 +3,7 @@ Copyright (c) 2018 Patrick Massot. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Patrick Massot, Johannes Hölzl
 -/
+import algebra.algebra.restrict_scalars
 import analysis.normed.field.basic
 import analysis.normed.group.infinite_sum
 import data.real.sqrt

src/topology/algebra/algebra.lean

@@ -6,6 +6,7 @@ Authors: Scott Morrison
 import algebra.algebra.subalgebra.basic
 import topology.algebra.module.basic
 import topology.algebra.field
+import ring_theory.adjoin.basic
 
 /-!
 # Topological (sub)algebras

src/topology/algebra/module/basic.lean

@@ -11,7 +11,6 @@ import topology.uniform_space.uniform_embedding
 import algebra.algebra.basic
 import linear_algebra.projection
 import linear_algebra.pi
-import linear_algebra.determinant
 import ring_theory.simple_module
 
 /-!
@@ -1319,12 +1318,6 @@ end smul_rightₗ
 
 section comm_ring
 
-/-- The determinant of a continuous linear map, mainly as a convenience device to be able to
-write `A.det` instead of `(A : M →ₗ[R] M).det`. -/
-@[reducible] noncomputable def det {R : Type*} [comm_ring R]
-  {M : Type*} [topological_space M] [add_comm_group M] [module R M] (A : M →L[R] M) : R :=
-linear_map.det (A : M →ₗ[R] M)
-
 variables
 {R : Type*} [comm_ring R]
 {M : Type*} [topological_space M] [add_comm_group M]
@@ -1938,11 +1931,6 @@ def fin_two_arrow : (fin 2 → M) ≃L[R] M × M :=
 
 end
 
-@[simp] lemma det_coe_symm {R : Type*} [field R]
-  {M : Type*} [topological_space M] [add_comm_group M] [module R M] (A : M ≃L[R] M) :
-  (A.symm : M →L[R] M).det = (A : M →L[R] M).det ⁻¹ :=
-linear_equiv.det_coe_symm A.to_linear_equiv
-
 end continuous_linear_equiv
 
 namespace continuous_linear_map

src/topology/algebra/module/determinant.lean

@@ -0,0 +1,31 @@
+/-
+Copyright (c) 2019 Sébastien Gouëzel. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Jan-David Salchow, Sébastien Gouëzel, Jean Lo, Yury Kudryashov, Frédéric Dupuis,
+  Heather Macbeth
+-/
+import topology.algebra.module.basic
+import linear_algebra.determinant
+
+/-!
+# The determinant of a continuous linear map.
+-/
+
+namespace continuous_linear_map
+
+/-- The determinant of a continuous linear map, mainly as a convenience device to be able to
+write `A.det` instead of `(A : M →ₗ[R] M).det`. -/
+@[reducible] noncomputable def det {R : Type*} [comm_ring R]
+  {M : Type*} [topological_space M] [add_comm_group M] [module R M] (A : M →L[R] M) : R :=
+linear_map.det (A : M →ₗ[R] M)
+
+end continuous_linear_map
+
+namespace continuous_linear_equiv
+
+@[simp] lemma det_coe_symm {R : Type*} [field R]
+  {M : Type*} [topological_space M] [add_comm_group M] [module R M] (A : M ≃L[R] M) :
+  (A.symm : M →L[R] M).det = (A : M →L[R] M).det ⁻¹ :=
+linear_equiv.det_coe_symm A.to_linear_equiv
+
+end continuous_linear_equiv

src/topology/algebra/module/finite_dimension.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Sébastien Gouëzel, Anatole Dedecker
 -/
 import analysis.locally_convex.balanced_core_hull
+import topology.algebra.module.determinant
 
 /-!
 # Finite dimensional topological vector spaces over complete fields

src/topology/algebra/module/weak_dual.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Kalle Kytölä, Moritz Doll
 -/
 import topology.algebra.module.basic
+import linear_algebra.bilinear_map
 
 /-!
 # Weak dual topology