diff --git a/Mathlib.lean b/Mathlib.lean
index a7b8581722941a..fe782297dc14db 100644
--- a/Mathlib.lean
+++ b/Mathlib.lean
@@ -606,6 +606,7 @@ import Mathlib.Algebra.Polynomial.Inductions
 import Mathlib.Algebra.Polynomial.Laurent
 import Mathlib.Algebra.Polynomial.Lifts
 import Mathlib.Algebra.Polynomial.Mirror
+import Mathlib.Algebra.Polynomial.Module.AEval
 import Mathlib.Algebra.Polynomial.Module.Basic
 import Mathlib.Algebra.Polynomial.Module.FiniteDimensional
 import Mathlib.Algebra.Polynomial.Monic
diff --git a/Mathlib/Algebra/Polynomial/Derivation.lean b/Mathlib/Algebra/Polynomial/Derivation.lean
index 3f1810c04a5816..1ce37450b136aa 100644
--- a/Mathlib/Algebra/Polynomial/Derivation.lean
+++ b/Mathlib/Algebra/Polynomial/Derivation.lean
@@ -5,7 +5,7 @@ Authors: Kevin Buzzard, Richard Hill
 -/
 import Mathlib.Algebra.Polynomial.AlgebraMap
 import Mathlib.Algebra.Polynomial.Derivative
-import Mathlib.Algebra.Polynomial.Module.Basic
+import Mathlib.Algebra.Polynomial.Module.AEval
 import Mathlib.RingTheory.Derivation.Basic
 /-!
 # Derivations of univariate polynomials
diff --git a/Mathlib/Algebra/Polynomial/Module/AEval.lean b/Mathlib/Algebra/Polynomial/Module/AEval.lean
new file mode 100644
index 00000000000000..101d2de77a9a87
--- /dev/null
+++ b/Mathlib/Algebra/Polynomial/Module/AEval.lean
@@ -0,0 +1,197 @@
+/-
+Copyright (c) 2022 Richard M. Hill. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Richard M. Hill
+-/
+import Mathlib.Algebra.Polynomial.AlgebraMap
+import Mathlib.RingTheory.Finiteness
+
+/-!
+# Action of the polynomial ring on module induced by an algebra element.
+
+Given an element `a` in an `R`-algebra `A` and an `A`-module `M` we define an
+`R[X]`-module `Module.AEval R M a`, which is a type synonym of `M` with the
+action of a polynomial `f` given by `f • m = Polynomial.aeval a f • m`.
+In particular `X • m = a • m`.
+
+In the special case that `A = M →ₗ[R] M` and `φ : M →ₗ[R] M`, the module `Module.AEval R M a` is
+abbreviated `Module.AEval' φ`. In this module we have `X • m = ↑φ m`.
+-/
+
+open Set Function Polynomial
+
+namespace Module
+/--
+Suppose `a` is an element of an `R`-algebra `A` and `M` is an `A`-module.
+Loosely speaking, `Module.AEval R M a` is the `R[X]`-module with elements `m : M`,
+where the action of a polynomial $f$ is given by $f • m = f(a) • m$.
+
+More precisely, `Module.AEval R M a` has elements `Module.AEval.of R M a m` for `m : M`,
+and the action of `f` is `f • (of R M a m) = of R M a ((aeval a f) • m)`.
+-/
+@[nolint unusedArguments]
+def AEval (R M : Type*) {A : Type*} [CommSemiring R] [Semiring A] [Algebra R A]
+    [AddCommMonoid M] [Module A M] [Module R M] [IsScalarTower R A M] (_ : A) := M
+
+instance AEval.instAddCommGroup {R A M} [CommSemiring R] [Semiring A] (a : A) [Algebra R A]
+    [AddCommGroup M] [Module A M] [Module R M] [IsScalarTower R A M] :
+    AddCommGroup <| AEval R M a := inferInstanceAs (AddCommGroup M)
+
+variable {R A M} [CommSemiring R] [Semiring A] (a : A) [Algebra R A] [AddCommMonoid M] [Module A M]
+  [Module R M] [IsScalarTower R A M]
+
+namespace AEval
+
+instance instAddCommMonoid : AddCommMonoid <| AEval R M a := inferInstanceAs (AddCommMonoid M)
+
+instance instModuleOrig : Module R <| AEval R M a := inferInstanceAs (Module R M)
+
+instance instFiniteOrig [Finite R M] : Finite R <| AEval R M a := inferInstanceAs (Finite R M)
+
+instance instModulePolynomial : Module R[X] <| AEval R M a := compHom M (aeval a).toRingHom
+
+variable (R M)
+/--
+The canonical linear equivalence between `M` and `Module.AEval R M a` as an `R`-module.
+-/
+def of : M ≃ₗ[R] AEval R M a :=
+  LinearEquiv.refl _ _
+
+variable {R M}
+
+lemma of_aeval_smul (f : R[X]) (m : M) : of R M a (aeval a f • m) = f • of R M a m := rfl
+
+@[simp] lemma of_symm_smul (f : R[X]) (m : AEval R M a) :
+    (of R M a).symm (f • m) = aeval a f • (of R M a).symm m := rfl
+
+@[simp] lemma C_smul (t : R) (m : AEval R M a) : C t • m = t • m :=
+  (of R M a).symm.injective <| by simp
+
+lemma X_smul_of (m : M) : (X : R[X]) • (of R M a m) = of R M a (a • m) := by
+  rw [← of_aeval_smul, aeval_X]
+
+lemma of_symm_X_smul (m : AEval R M a) :
+    (of R M a).symm ((X : R[X]) • m) = a • (of R M a).symm m := by
+  rw [of_symm_smul, aeval_X]
+
+instance instIsScalarTowerOrigPolynomial : IsScalarTower R R[X] <| AEval R M a where
+  smul_assoc r f m := by
+    apply (of R M a).symm.injective
+    rw [of_symm_smul, map_smul, smul_assoc, map_smul, of_symm_smul]
+
+instance instFinitePolynomial [Finite R M] : Finite R[X] <| AEval R M a :=
+  Finite.of_restrictScalars_finite R _ _
+
+/-- Construct an `R[X]`-linear map out of `AEval R M a` from a `R`-linear map out of `M`. -/
+def _root_.LinearMap.ofAEval {N} [AddCommMonoid N] [Module R N] [Module R[X] N]
+    [IsScalarTower R R[X] N] (f : M →ₗ[R] N) (hf : ∀ m : M, f (a • m) = (X : R[X]) • f m) :
+    AEval R M a →ₗ[R[X]] N where
+  __ := f ∘ₗ (of R M a).symm
+  map_smul' p := p.induction_on (fun k m ↦ by simp [C_eq_algebraMap])
+    (fun p q hp hq m ↦ by simp_all [add_smul]) fun n k h m ↦ by
+      simp_rw [RingHom.id_apply, AddHom.toFun_eq_coe, LinearMap.coe_toAddHom,
+        LinearMap.comp_apply, LinearEquiv.coe_toLinearMap] at h ⊢
+      simp_rw [pow_succ, ← mul_assoc, mul_smul _ X, ← hf, ← of_symm_X_smul, ← h]
+
+lemma annihilator_eq_ker_aeval [FaithfulSMul A M] :
+    annihilator R[X] (AEval R M a) = RingHom.ker (aeval a) := by
+  ext p
+  simp_rw [mem_annihilator, RingHom.mem_ker]
+  change (∀ m : M, aeval a p • m = 0) ↔ _
+  exact ⟨fun h ↦ eq_of_smul_eq_smul (α := M) <| by simp [h], fun h ↦ by simp [h]⟩
+
+@[simp]
+lemma annihilator_top_eq_ker_aeval [FaithfulSMul A M] :
+    (⊤ : Submodule R[X] <| AEval R M a).annihilator = RingHom.ker (aeval a) := by
+  ext p
+  simp only [Submodule.mem_annihilator, Submodule.mem_top, forall_true_left, RingHom.mem_ker]
+  change (∀ m : M, aeval a p • m = 0) ↔ _
+  exact ⟨fun h ↦ eq_of_smul_eq_smul (α := M) <| by simp [h], fun h ↦ by simp [h]⟩
+
+section Submodule
+
+variable {p : Submodule R M} (hp : p ≤ p.comap (Algebra.lsmul R R M a))
+  {q : Submodule R[X] <| AEval R M a}
+
+variable (R M) in
+/-- We can turn an `R[X]`-submodule into an `R`-submodule by forgetting the action of `X`. -/
+def comapSubmodule :
+    CompleteLatticeHom (Submodule R[X] <| AEval R M a) (Submodule R M) :=
+  (Submodule.orderIsoMapComap (of R M a)).symm.toCompleteLatticeHom.comp <|
+    Submodule.restrictScalarsLatticeHom R R[X] (AEval R M a)
+
+@[simp] lemma mem_comapSubmodule {x : M} :
+    x ∈ comapSubmodule R M a q ↔ of R M a x ∈ q :=
+  Iff.rfl
+
+@[simp] lemma comapSubmodule_le_comap :
+    comapSubmodule R M a q ≤ (comapSubmodule R M a q).comap (Algebra.lsmul R R M a) := by
+  intro m hm
+  simpa only [Submodule.mem_comap, Algebra.lsmul_coe, mem_comapSubmodule, ← X_smul_of] using
+    q.smul_mem (X : R[X]) hm
+
+/-- An `R`-submodule which is stable under the action of `a` can be promoted to an
+`R[X]`-submodule. -/
+def mapSubmodule : Submodule R[X] <| AEval R M a :=
+  { toAddSubmonoid := p.toAddSubmonoid.map (of R M a)
+    smul_mem' := by
+      rintro f - ⟨m : M, h : m ∈ p, rfl⟩
+      simp only [AddSubsemigroup.mem_carrier, AddSubmonoid.mem_toSubsemigroup, AddSubmonoid.mem_map,
+        Submodule.mem_toAddSubmonoid]
+      exact ⟨aeval a f • m, aeval_apply_smul_mem_of_le_comap' h f a hp, of_aeval_smul a f m⟩ }
+
+@[simp] lemma mem_mapSubmodule {m : AEval R M a} :
+    m ∈ mapSubmodule a hp ↔ (of R M a).symm m ∈ p :=
+  ⟨fun ⟨_, hm, hm'⟩ ↦ hm'.symm ▸ hm, fun hm ↦ ⟨(of R M a).symm m, hm, rfl⟩⟩
+
+@[simp] lemma mapSubmodule_comapSubmodule (h := comapSubmodule_le_comap a) :
+    mapSubmodule a (p := comapSubmodule R M a q) h = q := by
+  ext; simp
+
+@[simp] lemma comapSubmodule_mapSubmodule :
+    comapSubmodule R M a (mapSubmodule a hp) = p := by
+  ext; simp
+
+variable (R M)
+
+lemma injective_comapSubmodule : Injective (comapSubmodule R M a) := by
+  intro q₁ q₂ hq
+  rw [← mapSubmodule_comapSubmodule (q := q₁), ← mapSubmodule_comapSubmodule (q := q₂)]
+  simp_rw [hq]
+
+lemma range_comapSubmodule :
+    range (comapSubmodule R M a) = {p | p ≤ p.comap (Algebra.lsmul R R M a)} :=
+  le_antisymm (fun _ ⟨_, hq⟩ ↦ hq ▸ comapSubmodule_le_comap a)
+    (fun _ hp ↦ ⟨mapSubmodule a hp, comapSubmodule_mapSubmodule a hp⟩)
+
+end Submodule
+
+end AEval
+
+variable (φ : M →ₗ[R] M)
+/--
+Given and `R`-module `M` and a linear map `φ : M →ₗ[R] M`, `Module.AEval' φ` is loosely speaking
+the `R[X]`-module with elements `m : M`, where the action of a polynomial $f$ is given by
+$f • m = f(a) • m$.
+
+More precisely, `Module.AEval' φ` has elements `Module.AEval'.of φ m` for `m : M`,
+and the action of `f` is `f • (of φ m) = of φ ((aeval φ f) • m)`.
+
+`Module.AEval'` is defined as a special case of `Module.AEval` in which the `R`-algebra is
+`M →ₗ[R] M`. Lemmas involving `Module.AEval` may be applied to `Module.AEval'`.
+-/
+abbrev AEval' := AEval R M φ
+/--
+The canonical linear equivalence between `M` and `Module.AEval' φ` as an `R`-module,
+where `φ : M →ₗ[R] M`.
+-/
+abbrev AEval'.of : M ≃ₗ[R] AEval' φ := AEval.of R M φ
+lemma AEval'_def : AEval' φ = AEval R M φ := rfl
+lemma AEval'.X_smul_of (m : M) : (X : R[X]) • AEval'.of φ m = AEval'.of φ (φ m) :=
+  AEval.X_smul_of _ _
+lemma AEval'.of_symm_X_smul (m : AEval' φ) :
+    (AEval'.of φ).symm ((X : R[X]) • m) = φ ((AEval'.of φ).symm m) := AEval.of_symm_X_smul _ _
+
+instance [Finite R M] : Finite R[X] <| AEval' φ := inferInstance
+
+end Module
diff --git a/Mathlib/Algebra/Polynomial/Module/Basic.lean b/Mathlib/Algebra/Polynomial/Module/Basic.lean
index a4964cb2f55c11..31f668479dc6c9 100644
--- a/Mathlib/Algebra/Polynomial/Module/Basic.lean
+++ b/Mathlib/Algebra/Polynomial/Module/Basic.lean
@@ -3,8 +3,7 @@ Copyright (c) 2022 Andrew Yang. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Andrew Yang
 -/
-import Mathlib.Algebra.Polynomial.AlgebraMap
-import Mathlib.RingTheory.Finiteness
+import Mathlib.Algebra.Polynomial.Module.AEval
 
 #align_import data.polynomial.module from "leanprover-community/mathlib"@"63417e01fbc711beaf25fa73b6edb395c0cfddd0"
 
@@ -15,192 +14,9 @@ In this file, we define the polynomial module for an `R`-module `M`, i.e. the `R
 
 This is defined as a type alias `PolynomialModule R M := ℕ →₀ M`, since there might be different
 module structures on `ℕ →₀ M` of interest. See the docstring of `PolynomialModule` for details.
-
-We also define, given an element `a` in an `R`-algebra `A` and an `A`-module `M`, an `R[X]`-module
-`Module.AEval R M a`, which is a type synonym of `M` with the action of a polynomial `f`
-given by `f • m = Polynomial.aeval a f • m`. In particular `X • m = a • m`.
-
-In the special case that `A = M →ₗ[R] M` and `φ : M →ₗ[R] M`, the module `Module.AEval R M a` is
-abbreviated `Module.AEval' φ`. In this module we have `X • m = ↑φ m`.
 -/
 universe u v
-open Set Function Polynomial
-
-namespace Module
-/--
-Suppose `a` is an element of an `R`-algebra `A` and `M` is an `A`-module.
-Loosely speaking, `Module.AEval R M a` is the `R[X]`-module with elements `m : M`,
-where the action of a polynomial $f$ is given by $f • m = f(a) • m$.
-
-More precisely, `Module.AEval R M a` has elements `Module.AEval.of R M a m` for `m : M`,
-and the action of `f` is `f • (of R M a m) = of R M a ((aeval a f) • m)`.
--/
-@[nolint unusedArguments]
-def AEval (R M : Type*) {A : Type*} [CommSemiring R] [Semiring A] [Algebra R A]
-    [AddCommMonoid M] [Module A M] [Module R M] [IsScalarTower R A M] (_ : A) := M
-
-instance AEval.instAddCommGroup {R A M} [CommSemiring R] [Semiring A] (a : A) [Algebra R A]
-    [AddCommGroup M] [Module A M] [Module R M] [IsScalarTower R A M] :
-    AddCommGroup <| AEval R M a := inferInstanceAs (AddCommGroup M)
-
-variable {R A M} [CommSemiring R] [Semiring A] (a : A) [Algebra R A] [AddCommMonoid M] [Module A M]
-  [Module R M] [IsScalarTower R A M]
-
-namespace AEval
-
-instance instAddCommMonoid : AddCommMonoid <| AEval R M a := inferInstanceAs (AddCommMonoid M)
-
-instance instModuleOrig : Module R <| AEval R M a := inferInstanceAs (Module R M)
-
-instance instFiniteOrig [Finite R M] : Finite R <| AEval R M a := inferInstanceAs (Finite R M)
-
-instance instModulePolynomial : Module R[X] <| AEval R M a := compHom M (aeval a).toRingHom
-
-variable (R M)
-/--
-The canonical linear equivalence between `M` and `Module.AEval R M a` as an `R`-module.
--/
-def of : M ≃ₗ[R] AEval R M a :=
-  LinearEquiv.refl _ _
-
-variable {R M}
-
-lemma of_aeval_smul (f : R[X]) (m : M) : of R M a (aeval a f • m) = f • of R M a m := rfl
-
-@[simp] lemma of_symm_smul (f : R[X]) (m : AEval R M a) :
-    (of R M a).symm (f • m) = aeval a f • (of R M a).symm m := rfl
-
-@[simp] lemma C_smul (t : R) (m : AEval R M a) : C t • m = t • m :=
-  (of R M a).symm.injective <| by simp
-
-lemma X_smul_of (m : M) : (X : R[X]) • (of R M a m) = of R M a (a • m) := by
-  rw [← of_aeval_smul, aeval_X]
-
-lemma of_symm_X_smul (m : AEval R M a) :
-    (of R M a).symm ((X : R[X]) • m) = a • (of R M a).symm m := by
-  rw [of_symm_smul, aeval_X]
-
-instance instIsScalarTowerOrigPolynomial : IsScalarTower R R[X] <| AEval R M a where
-  smul_assoc r f m := by
-    apply (of R M a).symm.injective
-    rw [of_symm_smul, map_smul, smul_assoc, map_smul, of_symm_smul]
-
-instance instFinitePolynomial [Finite R M] : Finite R[X] <| AEval R M a :=
-  Finite.of_restrictScalars_finite R _ _
-
-/-- Construct an `R[X]`-linear map out of `AEval R M a` from a `R`-linear map out of `M`. -/
-def _root_.LinearMap.ofAEval {N} [AddCommMonoid N] [Module R N] [Module R[X] N]
-    [IsScalarTower R R[X] N] (f : M →ₗ[R] N) (hf : ∀ m : M, f (a • m) = (X : R[X]) • f m) :
-    AEval R M a →ₗ[R[X]] N where
-  __ := f ∘ₗ (of R M a).symm
-  map_smul' p := p.induction_on (fun k m ↦ by simp [C_eq_algebraMap])
-    (fun p q hp hq m ↦ by simp_all [add_smul]) fun n k h m ↦ by
-      simp_rw [RingHom.id_apply, AddHom.toFun_eq_coe, LinearMap.coe_toAddHom,
-        LinearMap.comp_apply, LinearEquiv.coe_toLinearMap] at h ⊢
-      simp_rw [pow_succ, ← mul_assoc, mul_smul _ X, ← hf, ← of_symm_X_smul, ← h]
-
-lemma annihilator_eq_ker_aeval [FaithfulSMul A M] :
-    annihilator R[X] (AEval R M a) = RingHom.ker (aeval a) := by
-  ext p
-  simp_rw [mem_annihilator, RingHom.mem_ker]
-  change (∀ m : M, aeval a p • m = 0) ↔ _
-  exact ⟨fun h ↦ eq_of_smul_eq_smul (α := M) <| by simp [h], fun h ↦ by simp [h]⟩
-
-@[simp]
-lemma annihilator_top_eq_ker_aeval [FaithfulSMul A M] :
-    (⊤ : Submodule R[X] <| AEval R M a).annihilator = RingHom.ker (aeval a) := by
-  ext p
-  simp only [Submodule.mem_annihilator, Submodule.mem_top, forall_true_left, RingHom.mem_ker]
-  change (∀ m : M, aeval a p • m = 0) ↔ _
-  exact ⟨fun h ↦ eq_of_smul_eq_smul (α := M) <| by simp [h], fun h ↦ by simp [h]⟩
-
-section Submodule
-
-variable {p : Submodule R M} (hp : p ≤ p.comap (Algebra.lsmul R R M a))
-  {q : Submodule R[X] <| AEval R M a}
-
-variable (R M) in
-/-- We can turn an `R[X]`-submodule into an `R`-submodule by forgetting the action of `X`. -/
-def comapSubmodule :
-    CompleteLatticeHom (Submodule R[X] <| AEval R M a) (Submodule R M) :=
-  (Submodule.orderIsoMapComap (of R M a)).symm.toCompleteLatticeHom.comp <|
-    Submodule.restrictScalarsLatticeHom R R[X] (AEval R M a)
-
-@[simp] lemma mem_comapSubmodule {x : M} :
-    x ∈ comapSubmodule R M a q ↔ of R M a x ∈ q :=
-  Iff.rfl
-
-@[simp] lemma comapSubmodule_le_comap :
-    comapSubmodule R M a q ≤ (comapSubmodule R M a q).comap (Algebra.lsmul R R M a) := by
-  intro m hm
-  simpa only [Submodule.mem_comap, Algebra.lsmul_coe, mem_comapSubmodule, ← X_smul_of] using
-    q.smul_mem (X : R[X]) hm
-
-/-- An `R`-submodule which is stable under the action of `a` can be promoted to an
-`R[X]`-submodule. -/
-def mapSubmodule : Submodule R[X] <| AEval R M a :=
-  { toAddSubmonoid := p.toAddSubmonoid.map (of R M a)
-    smul_mem' := by
-      rintro f - ⟨m : M, h : m ∈ p, rfl⟩
-      simp only [AddSubsemigroup.mem_carrier, AddSubmonoid.mem_toSubsemigroup, AddSubmonoid.mem_map,
-        Submodule.mem_toAddSubmonoid]
-      exact ⟨aeval a f • m, aeval_apply_smul_mem_of_le_comap' h f a hp, of_aeval_smul a f m⟩ }
-
-@[simp] lemma mem_mapSubmodule {m : AEval R M a} :
-    m ∈ mapSubmodule a hp ↔ (of R M a).symm m ∈ p :=
-  ⟨fun ⟨_, hm, hm'⟩ ↦ hm'.symm ▸ hm, fun hm ↦ ⟨(of R M a).symm m, hm, rfl⟩⟩
-
-@[simp] lemma mapSubmodule_comapSubmodule (h := comapSubmodule_le_comap a) :
-    mapSubmodule a (p := comapSubmodule R M a q) h = q := by
-  ext; simp
-
-@[simp] lemma comapSubmodule_mapSubmodule :
-    comapSubmodule R M a (mapSubmodule a hp) = p := by
-  ext; simp
-
-variable (R M)
-
-lemma injective_comapSubmodule : Injective (comapSubmodule R M a) := by
-  intro q₁ q₂ hq
-  rw [← mapSubmodule_comapSubmodule (q := q₁), ← mapSubmodule_comapSubmodule (q := q₂)]
-  simp_rw [hq]
-
-lemma range_comapSubmodule :
-    range (comapSubmodule R M a) = {p | p ≤ p.comap (Algebra.lsmul R R M a)} :=
-  le_antisymm (fun _ ⟨_, hq⟩ ↦ hq ▸ comapSubmodule_le_comap a)
-    (fun _ hp ↦ ⟨mapSubmodule a hp, comapSubmodule_mapSubmodule a hp⟩)
-
-end Submodule
-
-end AEval
-
-variable (φ : M →ₗ[R] M)
-/--
-Given and `R`-module `M` and a linear map `φ : M →ₗ[R] M`, `Module.AEval' φ` is loosely speaking
-the `R[X]`-module with elements `m : M`, where the action of a polynomial $f$ is given by
-$f • m = f(a) • m$.
-
-More precisely, `Module.AEval' φ` has elements `Module.AEval'.of φ m` for `m : M`,
-and the action of `f` is `f • (of φ m) = of φ ((aeval φ f) • m)`.
-
-`Module.AEval'` is defined as a special case of `Module.AEval` in which the `R`-algebra is
-`M →ₗ[R] M`. Lemmas involving `Module.AEval` may be applied to `Module.AEval'`.
--/
-abbrev AEval' := AEval R M φ
-/--
-The canonical linear equivalence between `M` and `Module.AEval' φ` as an `R`-module,
-where `φ : M →ₗ[R] M`.
--/
-abbrev AEval'.of : M ≃ₗ[R] AEval' φ := AEval.of R M φ
-lemma AEval'_def : AEval' φ = AEval R M φ := rfl
-lemma AEval'.X_smul_of (m : M) : (X : R[X]) • AEval'.of φ m = AEval'.of φ (φ m) :=
-  AEval.X_smul_of _ _
-lemma AEval'.of_symm_X_smul (m : AEval' φ) :
-    (AEval'.of φ).symm ((X : R[X]) • m) = φ ((AEval'.of φ).symm m) := AEval.of_symm_X_smul _ _
-
-instance [Finite R M] : Finite R[X] <| AEval' φ := inferInstance
-
-end Module
+open Polynomial BigOperators
 
 /-- The `R[X]`-module `M[X]` for an `R`-module `M`.
 This is isomorphic (as an `R`-module) to `M[X]` when `M` is a ring.
diff --git a/Mathlib/Algebra/Polynomial/Module/FiniteDimensional.lean b/Mathlib/Algebra/Polynomial/Module/FiniteDimensional.lean
index 0cb6a4db253848..fc4eddf31558dd 100644
--- a/Mathlib/Algebra/Polynomial/Module/FiniteDimensional.lean
+++ b/Mathlib/Algebra/Polynomial/Module/FiniteDimensional.lean
@@ -3,9 +3,9 @@ Copyright (c) 2024 Oliver Nash. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Oliver Nash
 -/
-import Mathlib.Algebra.Polynomial.Module.Basic
 import Mathlib.FieldTheory.Minpoly.Field
 import Mathlib.LinearAlgebra.FiniteDimensional
+import Mathlib.Algebra.Polynomial.Module.AEval
 
 /-!
 # Polynomial modules in finite dimensions
diff --git a/Mathlib/LinearAlgebra/AnnihilatingPolynomial.lean b/Mathlib/LinearAlgebra/AnnihilatingPolynomial.lean
index 85f4e6efd54aaa..1990cf1bee3f92 100644
--- a/Mathlib/LinearAlgebra/AnnihilatingPolynomial.lean
+++ b/Mathlib/LinearAlgebra/AnnihilatingPolynomial.lean
@@ -5,7 +5,7 @@ Authors: Justin Thomas
 -/
 import Mathlib.FieldTheory.Minpoly.Field
 import Mathlib.RingTheory.PrincipalIdealDomain
-import Mathlib.Algebra.Polynomial.Module.Basic
+import Mathlib.Algebra.Polynomial.Module.AEval
 
 #align_import linear_algebra.annihilating_polynomial from "leanprover-community/mathlib"@"d3e8e0a0237c10c2627bf52c246b15ff8e7df4c0"