diff --git a/Mathlib.lean b/Mathlib.lean
index 34090017c1344..200f9867fde1f 100644
--- a/Mathlib.lean
+++ b/Mathlib.lean
@@ -2444,6 +2444,7 @@ import Mathlib.Data.Finsupp.Basic
 import Mathlib.Data.Finsupp.BigOperators
 import Mathlib.Data.Finsupp.Defs
 import Mathlib.Data.Finsupp.Encodable
+import Mathlib.Data.Finsupp.Ext
 import Mathlib.Data.Finsupp.Fin
 import Mathlib.Data.Finsupp.Fintype
 import Mathlib.Data.Finsupp.Indicator
diff --git a/Mathlib/Algebra/BigOperators/Finsupp.lean b/Mathlib/Algebra/BigOperators/Finsupp.lean
index dffd8f94b48be..aa65c1a7f1615 100644
--- a/Mathlib/Algebra/BigOperators/Finsupp.lean
+++ b/Mathlib/Algebra/BigOperators/Finsupp.lean
@@ -7,6 +7,7 @@ import Mathlib.Algebra.BigOperators.Pi
 import Mathlib.Algebra.BigOperators.Ring
 import Mathlib.Algebra.BigOperators.Fin
 import Mathlib.Algebra.Group.Submonoid.Membership
+import Mathlib.Data.Finsupp.Ext
 import Mathlib.Data.Finsupp.Fin
 import Mathlib.Data.Finsupp.Indicator
 
diff --git a/Mathlib/Data/Finsupp/Defs.lean b/Mathlib/Data/Finsupp/Defs.lean
index be9894c31daf0..cc74d56fe7a74 100644
--- a/Mathlib/Data/Finsupp/Defs.lean
+++ b/Mathlib/Data/Finsupp/Defs.lean
@@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Johannes Hölzl, Kim Morrison
 -/
 import Mathlib.Algebra.Group.Indicator
-import Mathlib.Algebra.Group.Submonoid.Basic
 import Mathlib.Data.Finset.Max
 import Mathlib.Data.Set.Finite.Basic
 import Mathlib.Algebra.Group.TypeTags.Hom
@@ -81,6 +80,7 @@ This file is a `noncomputable theory` and uses classical logic throughout.
 
 -/
 
+assert_not_exists Submonoid
 
 noncomputable section
 
@@ -1130,50 +1130,6 @@ theorem induction_on_min₂ (f : α →₀ M) (h0 : p 0)
 
 end LinearOrder
 
-@[simp]
-theorem add_closure_setOf_eq_single :
-    AddSubmonoid.closure { f : α →₀ M | ∃ a b, f = single a b } = ⊤ :=
-  top_unique fun x _hx =>
-    Finsupp.induction x (AddSubmonoid.zero_mem _) fun a b _f _ha _hb hf =>
-      AddSubmonoid.add_mem _ (AddSubmonoid.subset_closure <| ⟨a, b, rfl⟩) hf
-
-/-- If two additive homomorphisms from `α →₀ M` are equal on each `single a b`,
-then they are equal. -/
-theorem addHom_ext [AddZeroClass N] ⦃f g : (α →₀ M) →+ N⦄
-    (H : ∀ x y, f (single x y) = g (single x y)) : f = g := by
-  refine AddMonoidHom.eq_of_eqOn_denseM add_closure_setOf_eq_single ?_
-  rintro _ ⟨x, y, rfl⟩
-  apply H
-
-/-- If two additive homomorphisms from `α →₀ M` are equal on each `single a b`,
-then they are equal.
-
-We formulate this using equality of `AddMonoidHom`s so that `ext` tactic can apply a type-specific
-extensionality lemma after this one.  E.g., if the fiber `M` is `ℕ` or `ℤ`, then it suffices to
-verify `f (single a 1) = g (single a 1)`. -/
-@[ext high]
-theorem addHom_ext' [AddZeroClass N] ⦃f g : (α →₀ M) →+ N⦄
-    (H : ∀ x, f.comp (singleAddHom x) = g.comp (singleAddHom x)) : f = g :=
-  addHom_ext fun x => DFunLike.congr_fun (H x)
-
-theorem mulHom_ext [MulOneClass N] ⦃f g : Multiplicative (α →₀ M) →* N⦄
-    (H : ∀ x y, f (Multiplicative.ofAdd <| single x y) = g (Multiplicative.ofAdd <| single x y)) :
-    f = g :=
-  MonoidHom.ext <|
-    DFunLike.congr_fun <| by
-      have := @addHom_ext α M (Additive N) _ _
-        (MonoidHom.toAdditive'' f) (MonoidHom.toAdditive'' g) H
-      ext
-      rw [DFunLike.ext_iff] at this
-      apply this
-
-@[ext]
-theorem mulHom_ext' [MulOneClass N] {f g : Multiplicative (α →₀ M) →* N}
-    (H : ∀ x, f.comp (AddMonoidHom.toMultiplicative (singleAddHom x)) =
-              g.comp (AddMonoidHom.toMultiplicative (singleAddHom x))) :
-    f = g :=
-  mulHom_ext fun x => DFunLike.congr_fun (H x)
-
 theorem mapRange_add [AddZeroClass N] {f : M → N} {hf : f 0 = 0}
     (hf' : ∀ x y, f (x + y) = f x + f y) (v₁ v₂ : α →₀ M) :
     mapRange f hf (v₁ + v₂) = mapRange f hf v₁ + mapRange f hf v₂ :=
diff --git a/Mathlib/Data/Finsupp/Ext.lean b/Mathlib/Data/Finsupp/Ext.lean
new file mode 100644
index 0000000000000..fc184f2cf52f3
--- /dev/null
+++ b/Mathlib/Data/Finsupp/Ext.lean
@@ -0,0 +1,71 @@
+/-
+Copyright (c) 2017 Johannes Hölzl. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Johannes Hölzl, Kim Morrison
+-/
+import Mathlib.Algebra.Group.Submonoid.Basic
+import Mathlib.Data.Finsupp.Defs
+
+/-!
+# Extensionality for maps on `Finsupp`
+
+This file contains some extensionality principles for maps on `Finsupp`.
+These have been moved to their own file to avoid depending on submonoids when defining `Finsupp`.
+
+## Main results
+
+* `Finsupp.add_closure_setOf_eq_single`: `Finsupp` is generated by all the `single`s
+* `Finsupp.addHom_ext`: additive homomorphisms that are equal on each `single` are equal everywhere
+-/
+
+variable {α M N : Type*}
+
+namespace Finsupp
+
+variable [AddZeroClass M]
+
+@[simp]
+theorem add_closure_setOf_eq_single :
+    AddSubmonoid.closure { f : α →₀ M | ∃ a b, f = single a b } = ⊤ :=
+  top_unique fun x _hx =>
+    Finsupp.induction x (AddSubmonoid.zero_mem _) fun a b _f _ha _hb hf =>
+      AddSubmonoid.add_mem _ (AddSubmonoid.subset_closure <| ⟨a, b, rfl⟩) hf
+
+/-- If two additive homomorphisms from `α →₀ M` are equal on each `single a b`,
+then they are equal. -/
+theorem addHom_ext [AddZeroClass N] ⦃f g : (α →₀ M) →+ N⦄
+    (H : ∀ x y, f (single x y) = g (single x y)) : f = g := by
+  refine AddMonoidHom.eq_of_eqOn_denseM add_closure_setOf_eq_single ?_
+  rintro _ ⟨x, y, rfl⟩
+  apply H
+
+/-- If two additive homomorphisms from `α →₀ M` are equal on each `single a b`,
+then they are equal.
+
+We formulate this using equality of `AddMonoidHom`s so that `ext` tactic can apply a type-specific
+extensionality lemma after this one.  E.g., if the fiber `M` is `ℕ` or `ℤ`, then it suffices to
+verify `f (single a 1) = g (single a 1)`. -/
+@[ext high]
+theorem addHom_ext' [AddZeroClass N] ⦃f g : (α →₀ M) →+ N⦄
+    (H : ∀ x, f.comp (singleAddHom x) = g.comp (singleAddHom x)) : f = g :=
+  addHom_ext fun x => DFunLike.congr_fun (H x)
+
+theorem mulHom_ext [MulOneClass N] ⦃f g : Multiplicative (α →₀ M) →* N⦄
+    (H : ∀ x y, f (Multiplicative.ofAdd <| single x y) = g (Multiplicative.ofAdd <| single x y)) :
+    f = g :=
+  MonoidHom.ext <|
+    DFunLike.congr_fun <| by
+      have := @addHom_ext α M (Additive N) _ _
+        (MonoidHom.toAdditive'' f) (MonoidHom.toAdditive'' g) H
+      ext
+      rw [DFunLike.ext_iff] at this
+      apply this
+
+@[ext]
+theorem mulHom_ext' [MulOneClass N] {f g : Multiplicative (α →₀ M) →* N}
+    (H : ∀ x, f.comp (AddMonoidHom.toMultiplicative (singleAddHom x)) =
+              g.comp (AddMonoidHom.toMultiplicative (singleAddHom x))) :
+    f = g :=
+  mulHom_ext fun x => DFunLike.congr_fun (H x)
+
+end Finsupp