diff --git a/.github/workflows/01-claim-issue.yml b/.github/workflows/01-claim-issue.yml
index e78b5618..d8f6de7e 100644
--- a/.github/workflows/01-claim-issue.yml
+++ b/.github/workflows/01-claim-issue.yml
@@ -6,7 +6,7 @@ on:
 
 jobs:
   claim_issue:
-    if: github.event.issue.pull_request == null && contains(github.event.comment.body, 'claim')
+    if: github.event.issue.pull_request == null && contains(github.event.comment.body, 'claim') && !contains(github.event.comment.body, 'disclaim')
     runs-on: ubuntu-latest
 
     steps:
diff --git a/FLT/DivisionAlgebra/Finiteness.lean b/FLT/DivisionAlgebra/Finiteness.lean
index b6f23a51..41bee032 100644
--- a/FLT/DivisionAlgebra/Finiteness.lean
+++ b/FLT/DivisionAlgebra/Finiteness.lean
@@ -8,7 +8,7 @@ import Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Basic
 import Mathlib.NumberTheory.NumberField.Basic
 import Mathlib.RingTheory.DedekindDomain.FiniteAdeleRing
 import Mathlib.Algebra.Group.Subgroup.Pointwise
-import FLT.ForMathlib.ActionTopology
+import FLT.Mathlib.Topology.Algebra.Module.ModuleTopology
 import FLT.NumberField.IsTotallyReal
 import FLT.NumberField.AdeleRing
 import Mathlib.GroupTheory.DoubleCoset
@@ -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) _
+  IsModuleTopology.Module.topologicalRing (FiniteAdeleRing (𝓞 K) K) _
 
 variable [Algebra.IsCentral K D]
 
diff --git a/FLT/FLT_files.lean b/FLT/FLT_files.lean
index 4837d633..bb9f21c0 100644
--- a/FLT/FLT_files.lean
+++ b/FLT/FLT_files.lean
@@ -5,11 +5,8 @@ import FLT.Basic.Reductions
 import FLT.DedekindDomain.FiniteAdeleRing.BaseChange
 import FLT.DivisionAlgebra.Finiteness
 import FLT.EllipticCurve.Torsion
-import FLT.ForMathlib.ActionTopology
-import FLT.ForMathlib.Algebra
 import FLT.ForMathlib.DomMulActMeasure
 import FLT.ForMathlib.MiscLemmas
-import FLT.FromMathlib.Algebra
 import FLT.GaloisRepresentation.Cyclotomic
 import FLT.GaloisRepresentation.HardlyRamified
 import FLT.GlobalLanglandsConjectures.GLnDefs
@@ -18,6 +15,12 @@ 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
+import FLT.Mathlib.Data.ENNReal.Inv
 import FLT.MathlibExperiments.Coalgebra.Monoid
 import FLT.MathlibExperiments.Coalgebra.Sweedler
 import FLT.MathlibExperiments.Coalgebra.TensorProduct
@@ -27,6 +30,8 @@ import FLT.MathlibExperiments.FrobeniusRiou
 import FLT.MathlibExperiments.HopfAlgebra.Basic
 import FLT.MathlibExperiments.IsCentralSimple
 import FLT.MathlibExperiments.IsFrobenius
+import FLT.Mathlib.Topology.Algebra.ContinuousAlgEquiv
+import FLT.Mathlib.Topology.Algebra.Module.ModuleTopology
 import FLT.NumberField.AdeleRing
 import FLT.NumberField.InfiniteAdeleRing
 import FLT.NumberField.IsTotallyReal
diff --git a/FLT/ForMathlib/MiscLemmas.lean b/FLT/ForMathlib/MiscLemmas.lean
index 40594900..79fd954e 100644
--- a/FLT/ForMathlib/MiscLemmas.lean
+++ b/FLT/ForMathlib/MiscLemmas.lean
@@ -27,6 +27,7 @@ theorem isOpenMap_of_coinduced (φ : A →+ B) (hφc : Continuous φ)
     rw [AddMonoidHom.map_add, hk, add_zero]
 
 -- **TODO** ask Yury how to golf
+-- Answer: `IsOpenQuotientMap.prodMap`
 open TopologicalSpace in
 theorem coinduced_prod_eq_prod_coinduced {X Y S T : Type*} [AddCommGroup X] [AddCommGroup Y]
     [AddCommGroup S] [AddCommGroup T] (f : X →+ S) (g : Y →+ T)
diff --git a/FLT/FromMathlib/Algebra.lean b/FLT/Junk/Algebra.lean
similarity index 99%
rename from FLT/FromMathlib/Algebra.lean
rename to FLT/Junk/Algebra.lean
index 6a4ef612..4a1ba097 100644
--- a/FLT/FromMathlib/Algebra.lean
+++ b/FLT/Junk/Algebra.lean
@@ -1,3 +1,4 @@
+#exit
 /-
 Copyright (c) 2024 Kevin Buzzard. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
diff --git a/FLT/ForMathlib/Algebra.lean b/FLT/Junk/Algebra2.lean
similarity index 100%
rename from FLT/ForMathlib/Algebra.lean
rename to FLT/Junk/Algebra2.lean
index cfc6820f..0372c3c4 100644
--- a/FLT/ForMathlib/Algebra.lean
+++ b/FLT/Junk/Algebra2.lean
@@ -1,5 +1,5 @@
-import Mathlib.RingTheory.OreLocalization.Ring
 #exit
+import Mathlib.RingTheory.OreLocalization.Ring
 
 -- extend localization theory to algebras
 -- I should only be doing this in the commutative case
diff --git a/FLT/ForMathlib/Topology/Algebra/Algebra.lean b/FLT/Mathlib/Topology/Algebra/ContinuousAlgEquiv.lean
similarity index 100%
rename from FLT/ForMathlib/Topology/Algebra/Algebra.lean
rename to FLT/Mathlib/Topology/Algebra/ContinuousAlgEquiv.lean
diff --git a/FLT/ForMathlib/ActionTopology.lean b/FLT/Mathlib/Topology/Algebra/Module/ModuleTopology.lean
similarity index 54%
rename from FLT/ForMathlib/ActionTopology.lean
rename to FLT/Mathlib/Topology/Algebra/Module/ModuleTopology.lean
index b8c26cd6..2c67f1c2 100644
--- a/FLT/ForMathlib/ActionTopology.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
@@ -14,25 +15,6 @@ This topology was suggested by Will Sawin [here](https://mathoverflow.net/a/4777
 
 ## Mathematical details
 
-I (buzzard) don't know of any reference for this other than Sawin's mathoverflow answer,
-so I expand some of the details here.
-
-First note that there *is* a finest topology with this property! Indeed, topologies on a fixed
-type form a complete lattice (infinite infs and sups exist). So if `τ` is the Inf of all
-the topologies on `A` which make `+` and `•` continuous, then the claim is that `+` and `•`
-are still continuous for `τ` (note that topologies are ordered so that finer topologies
-are smaller). To show `+ : A × A → A` is continuous we equivalently need to show
-that the pushforward of the product topology `τ × τ` along `+` is `≤ τ`, and because `τ` is
-the greatest lower bound of the topologies making `•` and `+` continuous,
-it suffices to show that it's `≤ σ` for any topology `σ` on `A` which makes `+` and `•` continuous.
-However pushforward and products are monotone, so `τ × τ ≤ σ × σ`, and the pushforward of
-`σ × σ` is `≤ σ` because that's precisely the statement that `+` is continuous for `σ`.
-The proof for `•` follows mutatis mutandis.
-
-A *topological module* for a topological ring `R` is an `R`-module `A` with a topology
-making `+` and `•` continuous. The discussion so far has shown that the action topology makes `A`
-into a topological module.
-
 A crucial observation is that if `M` is a topological `R`-module, if `A` is an `R`-module with no
 topology, and if `φ : A → M` is linear, then the pullback of `M`'s topology to `A` is a topology
 making `A` into a topological module. Let's for example check that `•` is continuous.
@@ -83,211 +65,31 @@ the corresponding statements in this file
 
 -/
 
-section basics
-
-/-
-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 IsModuleTopology
 
-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 ModuleTopology
 
 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] [TopologicalSpace A] [IsModuleTopology R A]
+variable {B : Type*} [AddCommGroup B] [Module R B] [τB : 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
+    Topology.IsQuotientMap φ := by
+  refine ⟨hφ, ?_⟩
+  haveI : ContinuousAdd A := toContinuousAdd R A
+  haveI : ContinuousAdd B := toContinuousAdd R B
   have : Continuous φ := continuous_of_linearMap φ
-  rw [continuous_iff_coinduced_le, isActionTopology R A, isActionTopology R B] at this
-  apply le_antisymm this
-  have : ContinuousAdd A := isActionTopology_continuousAdd R A
+  rw [continuous_iff_coinduced_le] at this
+  apply le_antisymm ?_ this
+  rw [eq_moduleTopology R B, eq_moduleTopology 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,26 +105,27 @@ 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] 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) ∘
       (Prod.map ⇑φ.toAddMonoidHom ⇑φ.toAddMonoidHom) by ext; simp, Set.preimage_comp] at bar
     clear! τB -- easiest to just remove topology on B completely now
+    rw [← eq_moduleTopology R A] at bar
     convert isOpenMap_of_coinduced (AddMonoidHom.prodMap φ.toAddMonoidHom φ.toAddMonoidHom)
       (_) (_) (_) 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 +133,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 +150,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 +170,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 +195,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 +219,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 +246,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 +278,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]
@@ -489,14 +292,13 @@ theorem Module.continuous_bilinear_of_finite [Module.Finite R A]
   have foo : Function.Surjective (LinearMap.id : B →ₗ[R] B) :=
     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]
+  have := (coinduced_of_surjective hφ).2
+  rw [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 [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 +317,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 +325,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 +340,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