diff --git a/FLT/DivisionAlgebra/Finiteness.lean b/FLT/DivisionAlgebra/Finiteness.lean
index afa15e47..1dca4305 100644
--- a/FLT/DivisionAlgebra/Finiteness.lean
+++ b/FLT/DivisionAlgebra/Finiteness.lean
@@ -34,14 +34,14 @@ variable (K : Type*) [Field K] [NumberField K]
 variable (D : Type*) [DivisionRing D] [Algebra K D]
 
 local instance : TopologicalSpace (FiniteAdeleRing (𝓞 K) K ⊗[K] D) :=
-  actionTopology (FiniteAdeleRing (𝓞 K) K) _
-local instance : IsActionTopology (FiniteAdeleRing (𝓞 K) K) ((FiniteAdeleRing (𝓞 K) K) ⊗[K] D) :=
+  moduleTopology (FiniteAdeleRing (𝓞 K) K) _
+local instance : IsModuleTopology (FiniteAdeleRing (𝓞 K) K) ((FiniteAdeleRing (𝓞 K) K) ⊗[K] D) :=
   ⟨rfl⟩
 
 variable [FiniteDimensional K D]
 
 instance : TopologicalRing ((FiniteAdeleRing (𝓞 K) K) ⊗[K] D) :=
-  ActionTopology.Module.topologicalRing (FiniteAdeleRing (𝓞 K) K) _
+  ModuleTopology.Module.topologicalRing (FiniteAdeleRing (𝓞 K) K) _
 
 variable [Algebra.IsCentral K D]
 
diff --git a/FLT/FLT_files.lean b/FLT/FLT_files.lean
index f6183473..bb9f21c0 100644
--- a/FLT/FLT_files.lean
+++ b/FLT/FLT_files.lean
@@ -15,6 +15,8 @@ import FLT.GroupScheme.FiniteFlat
 import FLT.HaarMeasure.DistribHaarChar
 import FLT.Hard.Results
 import FLT.HIMExperiments.flatness
+import FLT.Junk.Algebra
+import FLT.Junk.Algebra2
 import FLT.Mathlib.Algebra.Algebra.Subalgebra.Pi
 import FLT.Mathlib.Algebra.Order.Hom.Monoid
 import FLT.Mathlib.Algebra.Order.Monoid.Unbundled.TypeTags
diff --git a/FLT/Mathlib/Topology/Algebra/Module/ModuleTopology.lean b/FLT/Mathlib/Topology/Algebra/Module/ModuleTopology.lean
index b8c26cd6..485acb7b 100644
--- a/FLT/Mathlib/Topology/Algebra/Module/ModuleTopology.lean
+++ b/FLT/Mathlib/Topology/Algebra/Module/ModuleTopology.lean
@@ -1,6 +1,7 @@
 import FLT.ForMathlib.MiscLemmas
 import Mathlib.Topology.Algebra.Ring.Basic
 import Mathlib.LinearAlgebra.FreeModule.Finite.Basic
+import Mathlib.Topology.Algebra.Module.ModuleTopology
 
 /-!
 # An "action topology" for modules over a topological ring
@@ -83,211 +84,36 @@ the corresponding statements in this file
 
 -/
 
-section basics
+namespace ModuleTopology
 
-/-
-This section is just boilerplate, defining the action topology and making
-some infrastructure.
--/
-variable (R : Type*) [TopologicalSpace R] (A : Type*) [Add A] [SMul R A]
-
-/-- The action topology, for a module `A` over a topological ring `R`. It's the finest topology
-making addition and the `R`-action continuous, or equivalently the finest topology making `A`
-into a topological `R`-module. More precisely it's the Inf of the set of
-topologies with these properties; theorems `continuousSMul` and `continuousAdd` show
-that the action topology also has these properties. -/
-abbrev actionTopology : TopologicalSpace A :=
-  sInf {t | @ContinuousSMul R A _ _ t ∧ @ContinuousAdd A t _}
-
-/-- A class asserting that the topology on a module over a topological ring `R` is
-the action topology. See `actionTopology` for more discussion of the action topology. -/
-class IsActionTopology [τA : TopologicalSpace A] : Prop where
-  isActionTopology' : τA = actionTopology R A
-
-theorem isActionTopology [τA : TopologicalSpace A] [IsActionTopology R A] :
-    τA = actionTopology R A :=
-  IsActionTopology.isActionTopology' (R := R) (A := A)
-
-/-- Scalar multiplication `• : R × A → A` is continuous if `R` is a topological
-ring, and `A` is an `R` module with the action topology. -/
-theorem ActionTopology.continuousSMul : @ContinuousSMul R A _ _ (actionTopology R A) :=
-  -- Proof: We need to prove that the product topology is finer than the pullback
-  -- of the action topology. But the action topology is an Inf and thus a limit,
-  -- and pullback is a right adjoint, so it preserves limits.
-  -- We must thus show that the product topology is finer than an Inf, so it suffices
-  -- to show it's a lower bound, which is not hard. All this is wrapped into
-  -- `continuousSMul_sInf`.
-  continuousSMul_sInf <| fun _ _ ↦ by simp_all only [Set.mem_setOf_eq]
-
-/-- Addition `+ : A × A → A` is continuous if `R` is a topological
-ring, and `A` is an `R` module with the action topology. -/
-theorem ActionTopology.continuousAdd : @ContinuousAdd A (actionTopology R A) _ :=
-  continuousAdd_sInf <| fun _ _ ↦ by simp_all only [Set.mem_setOf_eq]
-
-instance instIsActionTopology_continuousSMul [TopologicalSpace A] [IsActionTopology R A] :
-    ContinuousSMul R A := isActionTopology R A ▸ ActionTopology.continuousSMul R A
-
-theorem isActionTopology_continuousAdd [TopologicalSpace A] [IsActionTopology R A] :
-    ContinuousAdd A := isActionTopology R A ▸ ActionTopology.continuousAdd R A
-
-theorem actionTopology_le [τA : TopologicalSpace A] [ContinuousSMul R A] [ContinuousAdd A] :
-    actionTopology R A ≤ τA := sInf_le ⟨‹ContinuousSMul R A›, ‹ContinuousAdd A›⟩
-
-end basics
-
-namespace ActionTopology
-
-section zero
-
-instance instSubsingleton (R : Type*) [TopologicalSpace R] (A : Type*) [Add A] [SMul R A]
-    [Subsingleton A] [TopologicalSpace A] : IsActionTopology R A where
-  isActionTopology' := by
-    ext U
-    simp only [isOpen_discrete]
-
-end zero
-
-
-section one
-
-/-
-
-We now fix once and for all a topological semiring `R`.
-
-We first prove that the action topology on `R` considered as a module over itself,
-is `R`'s topology.
-
--/
-instance instSelf (R : Type*) [Semiring R] [τR : TopologicalSpace R] [TopologicalSemiring R] :
-    IsActionTopology R R := by
-  constructor
-  /- Let `R` be a topological ring with topology τR. To prove that `τR` is the action
-  topology, it suffices to prove inclusions in both directions.
-  One way is obvious: addition and multiplication are continuous for `R`, so the
-  action topology is finer than `R` because it's the finest topology with these properties.-/
-  refine le_antisymm ?_ (actionTopology_le R R)
-  /- The other way is more interesting. We can interpret the problem as proving that
-  the identity function is continuous from `R` with the action topology to `R` with
-  its usual topology to `R` with the action topology.
-  -/
-  rw [← continuous_id_iff_le]
-  /-
-  The idea needed here is to rewrite the identity function as the composite of `r ↦ (r,1)`
-  from `R` to `R × R`, and multiplication on `R × R`, where we topologise `R × R`
-  by giving the first `R` the usual topology and the second `R` the action topology.
-  -/
-  rw [show (id : R → R) = (fun rs ↦ rs.1 • rs.2) ∘ (fun r ↦ (r, 1)) by ext; simp]
-  /-
-  It thus suffices to show that each of these maps are continuous.
-  -/
-  apply @Continuous.comp R (R × R) R τR (@instTopologicalSpaceProd R R τR (actionTopology R R))
-      (actionTopology R R)
-  · /-
-    The map R × R → R is `•`, so by a fundamental property of the action topology,
-    this is continuous. -/
-    exact @continuous_smul _ _ _ _ (actionTopology R R) <| ActionTopology.continuousSMul ..
-  · /-
-    The map `R → R × R` sending `r` to `(r,1)` is a map into a product, so it suffices to show
-    that each of the two factors is continuous. But the first is the identity function and the
-    second is a constant function. -/
-    exact @Continuous.prod_mk _ _ _ _ (actionTopology R R) _ _ _ continuous_id <|
-      @continuous_const _ _ _ (actionTopology R R) _
-
-end one
-
-section iso
-
-variable {R : Type*} [τR : TopologicalSpace R] [Semiring R]
-variable {A : Type*} [AddCommMonoid A] [Module R A] [τA : TopologicalSpace A] [IsActionTopology R A]
-variable {B : Type*} [AddCommMonoid B] [Module R B] [τB : TopologicalSpace B]
-
-theorem iso (e : A ≃L[R] B) : IsActionTopology R B where
-  isActionTopology' := by
-    -- get these in before I start putting new topologies on A and B
-    let g : A →[R] B := e.toMulActionHom
-    let g' : B →[R] A := e.symm.toMulActionHom
-    let h : A →+ B := e
-    let h' : B →+ A := e.symm
-    simp_rw [e.toHomeomorph.symm.isInducing.1, isActionTopology R A, actionTopology, induced_sInf]
-    congr 1
-    ext τ
-    rw [Set.mem_image]
-    -- it's the same picture
-    constructor
-    · rintro ⟨σ, ⟨hσ1, hσ2⟩, rfl⟩
-      refine ⟨?_, ?_⟩
-      · exact induced_continuous_smul (f := @id R) (hf := continuous_id) (g := g') (τA := σ)
-      · exact induced_continuous_add (h := h')
-    · rintro ⟨h1, h2⟩
-      use τ.induced e
-      rw [induced_compose]
-      refine ⟨⟨?_, ?_⟩, ?_⟩
-      · exact induced_continuous_smul (f := @id R) (hf := continuous_id) (g := g) (τA := τ)
-      · exact induced_continuous_add (h := h)
-      · nth_rw 2 [← induced_id (t := τ)]
-        simp
-
-end iso
-
-section function
-
-variable {R : Type*} [τR : TopologicalSpace R] [Semiring R]
-variable {A : Type*} [AddCommMonoid A] [Module R A] [aA : TopologicalSpace A] [IsActionTopology R A]
-variable {B : Type*} [AddCommMonoid B] [Module R B] [aB : TopologicalSpace B]
-    [ContinuousAdd B] [ContinuousSMul R B]
-
-/-- Every `R`-linear map between two topological `R`-modules, where the source has the action
-topology, is continuous. -/
-@[fun_prop, continuity]
-theorem continuous_of_distribMulActionHom (φ : A →+[R] B) : Continuous φ := by
-  -- the proof: We know that `+ : B × B → B` and `• : R × B → B` are continuous for the action
-  -- topology on `B`, and two earlier theorems (`induced_continuous_smul` and
-  -- `induced_continuous_add`) say that hence `+` and `•` on `A` are continuous if `A`
-  -- is given the topology induced from `φ`. Hence the action topology is finer than
-  -- the induced topology, and so the function is continuous.
-  rw [isActionTopology R A, continuous_iff_le_induced]
-  --haveI : ContinuousAdd B := isActionTopology_continuousAdd R B
-  exact sInf_le <| ⟨induced_continuous_smul (φ.toMulActionHom) continuous_id,
-    induced_continuous_add φ.toAddMonoidHom⟩
-
-@[fun_prop, continuity]
-theorem continuous_of_linearMap (φ : A →ₗ[R] B) : Continuous φ :=
-  continuous_of_distribMulActionHom φ.toDistribMulActionHom
-
-variable (R) in
-theorem continuous_neg (C : Type*) [AddCommGroup C] [Module R C] [TopologicalSpace C]
-    [IsActionTopology R C] : Continuous (fun a ↦ -a : C → C) :=
-  haveI : ContinuousAdd C := isActionTopology_continuousAdd R C
-  continuous_of_linearMap (LinearEquiv.neg R).toLinearMap
-
-end function
+open IsModuleTopology
 
 section surjection
 
 variable {R : Type*} [τR : TopologicalSpace R] [Ring R] [TopologicalRing R]
-variable {A : Type*} [AddCommGroup A] [Module R A] --[aA : TopologicalSpace A] [IsActionTopology R A]
-variable {B : Type*} [AddCommGroup B] [Module R B] --[aB : TopologicalSpace B] [IsActionTopology R B]
+variable {A : Type*} [AddCommGroup A] [Module R A] --[aA : TopologicalSpace A] [IsModuleTopology R A]
+variable {B : Type*} [AddCommGroup B] [Module R B] --[aB : TopologicalSpace B] [IsModuleTopology R B]
 
 -- Here I need the lemma about how quotients are open so I do need groups
 -- because this relies on translates of an open being open
 theorem coinduced_of_surjective {φ : A →ₗ[R] B} (hφ : Function.Surjective φ) :
-    TopologicalSpace.coinduced φ (actionTopology R A) = actionTopology R B := by
-  letI : TopologicalSpace A := actionTopology R A
-  letI τB : TopologicalSpace B := actionTopology R B
-  haveI : IsActionTopology R A := ⟨rfl⟩
-  haveI : ContinuousAdd A := isActionTopology_continuousAdd R A
-  haveI : IsActionTopology R B := ⟨rfl⟩
-  haveI : ContinuousAdd B := isActionTopology_continuousAdd R B
+    TopologicalSpace.coinduced φ (moduleTopology R A) = moduleTopology R B := by
+  letI : TopologicalSpace A := moduleTopology R A
+  letI τB : TopologicalSpace B := moduleTopology R B
+  haveI : IsModuleTopology R A := ⟨rfl⟩
+  haveI : ContinuousAdd A := continuousAdd R A
+  haveI : IsModuleTopology R B := ⟨rfl⟩
+  haveI : ContinuousAdd B := continuousAdd R B
   have : Continuous φ := continuous_of_linearMap φ
-  rw [continuous_iff_coinduced_le, isActionTopology R A, isActionTopology R B] at this
+  rw [continuous_iff_coinduced_le, eq_moduleTopology R A, eq_moduleTopology R B] at this
   apply le_antisymm this
-  have : ContinuousAdd A := isActionTopology_continuousAdd R A
+  have : ContinuousAdd A := continuousAdd R A
   refine sInf_le ⟨?_, ?_⟩
   · apply @ContinuousSMul.mk R B _ _ (_)
     obtain ⟨foo⟩ : ContinuousSMul R A := inferInstance
     rw [continuous_def] at foo ⊢
     intro U hU
-    rw [isOpen_coinduced, ← isActionTopology R A] at hU
+    rw [isOpen_coinduced, ← eq_moduleTopology R A] at hU
     specialize foo _ hU; clear hU
     rw [← Set.preimage_comp, show φ ∘ (fun p ↦ p.1 • p.2 : R × A → A) =
       (fun p ↦ p.1 • p.2 : R × B → B) ∘
@@ -303,15 +129,15 @@ theorem coinduced_of_surjective {φ : A →ₗ[R] B} (hφ : Function.Surjective
       exact ⟨Function.surjective_id, by simp_all⟩
     · -- should `apply continuousprodmap ctrl-space` find `Continuous.prod_map`?
       apply @Continuous.prodMap _ _ _ _ (_) (_) (_) (_) id φ continuous_id
-      rw [continuous_iff_coinduced_le, isActionTopology R A]
-    · rw [← isActionTopology R A]
+      rw [continuous_iff_coinduced_le, eq_moduleTopology R A]
+    · rw [← eq_moduleTopology R A]
       exact coinduced_prod_eq_prod_coinduced (AddMonoidHom.id R) φ.toAddMonoidHom
        (Function.surjective_id) hφ
   · apply @ContinuousAdd.mk _ (_)
-    obtain ⟨bar⟩ := isActionTopology_continuousAdd R A
+    obtain ⟨bar⟩ := continuousAdd R A
     rw [continuous_def] at bar ⊢
     intro U hU
-    rw [isOpen_coinduced, ← isActionTopology R A] at hU
+    rw [isOpen_coinduced, ← eq_moduleTopology R A] at hU
     specialize bar _ hU; clear hU
     rw [← Set.preimage_comp, show φ ∘ (fun p ↦ p.1 + p.2 : A × A → A) =
       (fun p ↦ p.1 + p.2 : B × B → B) ∘
@@ -321,8 +147,8 @@ theorem coinduced_of_surjective {φ : A →ₗ[R] B} (hφ : Function.Surjective
       (_) (_) (_) bar
     · aesop
     · apply @Continuous.prodMap _ _ _ _ (_) (_) (_) (_) <;>
-      · rw [continuous_iff_coinduced_le, isActionTopology R A]; rfl
-    · rw [← isActionTopology R A]
+      · rw [continuous_iff_coinduced_le, eq_moduleTopology R A]; rfl
+    · rw [← eq_moduleTopology R A]
       exact coinduced_prod_eq_prod_coinduced (X := A) (Y := A) (S := B) (T := B) φ φ hφ hφ
 
 end surjection
@@ -330,13 +156,13 @@ end surjection
 section prod
 
 variable {R : Type*} [TopologicalSpace R] [Semiring R] [TopologicalSemiring R]
-variable {M : Type*} [AddCommMonoid M] [Module R M] [TopologicalSpace M] [IsActionTopology R M]
-variable {N : Type*} [AddCommMonoid N] [Module R N] [TopologicalSpace N] [IsActionTopology R N]
+variable {M : Type*} [AddCommMonoid M] [Module R M] [TopologicalSpace M] [IsModuleTopology R M]
+variable {N : Type*} [AddCommMonoid N] [Module R N] [TopologicalSpace N] [IsModuleTopology R N]
 
-instance prod : IsActionTopology R (M × N) := by
+instance prod : IsModuleTopology R (M × N) := by
   constructor
-  haveI : ContinuousAdd M := isActionTopology_continuousAdd R M
-  haveI : ContinuousAdd N := isActionTopology_continuousAdd R N
+  haveI : ContinuousAdd M := toContinuousAdd R M
+  haveI : ContinuousAdd N := toContinuousAdd R N
   refine le_antisymm ?_ <| sInf_le ⟨Prod.continuousSMul, Prod.continuousAdd⟩
   rw [← continuous_id_iff_le]
   rw [show (id : M × N → M × N) =
@@ -347,16 +173,16 @@ instance prod : IsActionTopology R (M × N) := by
   -- to always put the product topology on M × N, when we sometimes want the action topology
   -- (they are equal, but that's exactly what we're proving so we can't assume it yet).
   -- This issue stops the standard continuity tactics from working.
-  obtain ⟨this⟩ : @ContinuousAdd (M × N) (actionTopology R (M × N)) _ :=
-    ActionTopology.continuousAdd _ _
+  obtain ⟨this⟩ : @ContinuousAdd (M × N) (moduleTopology R (M × N)) _ :=
+    ModuleTopology.continuousAdd _ _
   refine @Continuous.comp _ ((M × N) × (M × N)) _ (_) (_) (_) _ _ this ?_
-  haveI : @ContinuousSMul R (M × N) _ _ (actionTopology R _) := continuousSMul R (M × N)
+  haveI : @ContinuousSMul R (M × N) _ _ (moduleTopology R _) := continuousSMul R (M × N)
   refine (@continuous_prod_mk _ _ _ (_) (_) (_) _ _).2 ⟨?_, ?_⟩
   · refine @Continuous.comp _ _ _ (_) (_) (_) _ ((LinearMap.inl R M N)) ?_ continuous_fst
-    apply @continuous_of_linearMap _ _ _ _ _ _ _ _ _ _ _ (actionTopology _ _) (?_)
+    apply @continuous_of_linearMap _ _ _ _ _ _ _ _ _ _ _ (moduleTopology _ _) (?_)
     exact continuousAdd R (M × N)
   · refine @Continuous.comp _ _ _ (_) (_) (_) _ ((LinearMap.inr R M N)) ?_ continuous_snd
-    apply @continuous_of_linearMap _ _ _ _ _ _ _ _ _ _ _ (actionTopology _ _) (?_)
+    apply @continuous_of_linearMap _ _ _ _ _ _ _ _ _ _ _ (moduleTopology _ _) (?_)
     exact continuousAdd R (M × N)
 
 end prod
@@ -367,7 +193,7 @@ variable {R : Type*} [τR : TopologicalSpace R] [Semiring R] [TopologicalSemirin
 
 variable {ι : Type*} [Finite ι] {A : ι → Type*} [∀ i, AddCommMonoid (A i)]
   [∀ i, Module R (A i)] [∀ i, TopologicalSpace (A i)]
-  [∀ i, IsActionTopology R (A i)]
+  [∀ i, IsModuleTopology R (A i)]
 
 -- elsewhere
 def ContinuousLinearEquiv.piCongrLeft (R : Type*) [Semiring R] {ι ι' : Type*}
@@ -392,7 +218,7 @@ def ContinuousLinearEquiv.pUnitPiEquiv (R : Type*) [Semiring R] (f : PUnit → T
   __ := LinearEquiv.pUnitPiEquiv R f
   __ := Homeomorph.pUnitPiEquiv f
 
-instance pi : IsActionTopology R (∀ i, A i) := by
+instance pi : IsModuleTopology R (∀ i, A i) := by
   induction ι using Finite.induction_empty_option
   · case of_equiv X Y e _ _ _ _ _ =>
     exact iso (ContinuousLinearEquiv.piCongrLeft R A e)
@@ -416,9 +242,9 @@ section semiring_bilinear
 variable {R : Type*} [τR : TopologicalSpace R] [CommSemiring R]
 
 -- similarly these don't need to be groups
-variable {A : Type*} [AddCommGroup A] [Module R A] [aA : TopologicalSpace A] [IsActionTopology R A]
-variable {B : Type*} [AddCommGroup B] [Module R B] [aB : TopologicalSpace B] [IsActionTopology R B]
-variable {C : Type*} [AddCommGroup C] [Module R C] [aC : TopologicalSpace C] [IsActionTopology R C]
+variable {A : Type*} [AddCommGroup A] [Module R A] [aA : TopologicalSpace A] [IsModuleTopology R A]
+variable {B : Type*} [AddCommGroup B] [Module R B] [aB : TopologicalSpace B] [IsModuleTopology R B]
+variable {C : Type*} [AddCommGroup C] [Module R C] [aC : TopologicalSpace C] [IsModuleTopology R C]
 
 theorem Module.continuous_bilinear_of_pi_finite (ι : Type*) [Finite ι]
     (bil : (ι → R) →ₗ[R] B →ₗ[R] C) : Continuous (fun ab ↦ bil ab.1 ab.2 : ((ι → R) × B → C)) := by
@@ -443,7 +269,7 @@ theorem Module.continuous_bilinear_of_pi_finite (ι : Type*) [Finite ι]
       simp
     · apply Set.toFinite _--(Function.support fun x ↦ f x • Pi.single x 1)
   rw [foo]
-  haveI : ContinuousAdd C := isActionTopology_continuousAdd R C
+  haveI : ContinuousAdd C := toContinuousAdd R C
   apply continuous_finsum (fun i ↦ by fun_prop)
   intro x
   use Set.univ
@@ -475,9 +301,9 @@ section ring_bilinear
 
 variable {R : Type*} [τR : TopologicalSpace R] [CommRing R] [TopologicalRing R]
 
-variable {A : Type*} [AddCommGroup A] [Module R A] [aA : TopologicalSpace A] [IsActionTopology R A]
-variable {B : Type*} [AddCommGroup B] [Module R B] [aB : TopologicalSpace B] [IsActionTopology R B]
-variable {C : Type*} [AddCommGroup C] [Module R C] [aC : TopologicalSpace C] [IsActionTopology R C]
+variable {A : Type*} [AddCommGroup A] [Module R A] [aA : TopologicalSpace A] [IsModuleTopology R A]
+variable {B : Type*} [AddCommGroup B] [Module R B] [aB : TopologicalSpace B] [IsModuleTopology R B]
+variable {C : Type*} [AddCommGroup C] [Module R C] [aC : TopologicalSpace C] [IsModuleTopology R C]
 
 -- This needs rings though
 theorem Module.continuous_bilinear_of_finite [Module.Finite R A]
@@ -490,13 +316,13 @@ theorem Module.continuous_bilinear_of_finite [Module.Finite R A]
     Function.RightInverse.surjective (congrFun rfl)
   have hφ : Function.Surjective φ := Function.Surjective.prodMap hf foo
   have := coinduced_of_surjective hφ
-  rw [isActionTopology R (A × B), ← this, continuous_def]
+  rw [eq_moduleTopology R (A × B), ← this, continuous_def]
   intro U hU
   rw [isOpen_coinduced, ← Set.preimage_comp]
   suffices Continuous ((fun ab ↦ (bil ab.1) ab.2) ∘ φ : (Fin m → R) × B → C) by
     rw [continuous_def] at this
     convert this _ hU
-    rw [← prod.isActionTopology']
+    rw [← prod.eq_moduleTopology']
   rw [show (fun ab ↦ (bil ab.1) ab.2 : A × B → C) ∘ φ = (fun fb ↦ bil' fb.1 fb.2) by
     ext ⟨a, b⟩
     simp [bil', φ]]
@@ -515,7 +341,7 @@ open scoped NumberField
 -- these shouldn't be rings, they should be semirings
 variable (R) [CommRing R] [TopologicalSpace R] [TopologicalRing R]
 variable (D : Type*) [Ring D] [Algebra R D] [Module.Finite R D] [Module.Free R D]
-variable [TopologicalSpace D] [IsActionTopology R D]
+variable [TopologicalSpace D] [IsModuleTopology R D]
 
 open scoped TensorProduct
 
@@ -523,11 +349,11 @@ open scoped TensorProduct
 theorem continuous_mul'
     (R : Type*) [CommRing R] [TopologicalSpace R] [TopologicalRing R]
     (D : Type*) [Ring D] [Algebra R D] [Module.Finite R D] [Module.Free R D] [TopologicalSpace D]
-    [IsActionTopology R D] : Continuous (fun ab ↦ ab.1 * ab.2 : D × D → D) :=
+    [IsModuleTopology R D] : Continuous (fun ab ↦ ab.1 * ab.2 : D × D → D) :=
   Module.continuous_bilinear_of_finite (LinearMap.mul R D)
 
 def topologicalSemiring : TopologicalSemiring D where
-  continuous_add := (isActionTopology_continuousAdd R D).1
+  continuous_add := (toContinuousAdd R D).1
   continuous_mul := continuous_mul' R D
 
 end semiring_algebra
@@ -538,19 +364,19 @@ section ring_algebra
 -- Is it: for D finite free R can be a semiring but for D finite it has to be a ring?
 variable (R) [CommRing R] [TopologicalSpace R] [TopologicalRing R]
 variable (D : Type*) [Ring D] [Algebra R D] [Module.Finite R D]
-variable [TopologicalSpace D] [IsActionTopology R D]
+variable [TopologicalSpace D] [IsModuleTopology R D]
 
 open scoped TensorProduct
 
 include R in
 @[continuity, fun_prop]
 theorem continuous_mul : Continuous (fun ab ↦ ab.1 * ab.2 : D × D → D) := by
-  letI : TopologicalSpace (D ⊗[R] D) := actionTopology R _
-  haveI : IsActionTopology R (D ⊗[R] D) := { isActionTopology' := rfl }
+  letI : TopologicalSpace (D ⊗[R] D) := moduleTopology R _
+  haveI : IsModuleTopology R (D ⊗[R] D) := { eq_moduleTopology' := rfl }
   convert Module.continuous_bilinear_of_finite <| (LinearMap.mul R D : D →ₗ[R] D →ₗ[R] D)
 
 def Module.topologicalRing : TopologicalRing D where
-  continuous_add := (isActionTopology_continuousAdd R D).1
+  continuous_add := (toContinuousAdd R D).1
   continuous_mul := continuous_mul R D
   continuous_neg := continuous_neg R D