diff --git a/Mathlib.lean b/Mathlib.lean
index 5e0aee1763797..55552ad2a0f9b 100644
--- a/Mathlib.lean
+++ b/Mathlib.lean
@@ -321,7 +321,9 @@ import Mathlib.Algebra.Group.Subsemigroup.Membership
 import Mathlib.Algebra.Group.Subsemigroup.Operations
 import Mathlib.Algebra.Group.Support
 import Mathlib.Algebra.Group.Translate
-import Mathlib.Algebra.Group.TypeTags
+import Mathlib.Algebra.Group.TypeTags.Basic
+import Mathlib.Algebra.Group.TypeTags.Finite
+import Mathlib.Algebra.Group.TypeTags.Hom
 import Mathlib.Algebra.Group.ULift
 import Mathlib.Algebra.Group.UniqueProds.Basic
 import Mathlib.Algebra.Group.UniqueProds.VectorSpace
diff --git a/Mathlib/Algebra/Category/Grp/FiniteGrp.lean b/Mathlib/Algebra/Category/Grp/FiniteGrp.lean
index b1f4d7ead61ee..ac01e3ac8ce3c 100644
--- a/Mathlib/Algebra/Category/Grp/FiniteGrp.lean
+++ b/Mathlib/Algebra/Category/Grp/FiniteGrp.lean
@@ -3,6 +3,7 @@ Copyright (c) 2024 Jujian Zhang. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Jujian Zhang, Nailin Guan, Yuyang Zhao
 -/
+import Mathlib.Data.Finite.Defs
 import Mathlib.Algebra.Category.Grp.Basic
 
 /-!
diff --git a/Mathlib/Algebra/FreeMonoid/Count.lean b/Mathlib/Algebra/FreeMonoid/Count.lean
index df4dcfd27f672..53b2c0e4c51c3 100644
--- a/Mathlib/Algebra/FreeMonoid/Count.lean
+++ b/Mathlib/Algebra/FreeMonoid/Count.lean
@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yury Kudryashov
 -/
 import Mathlib.Algebra.FreeMonoid.Basic
+import Mathlib.Algebra.Group.TypeTags.Hom
 
 /-!
 # `List.count` as a bundled homomorphism
diff --git a/Mathlib/Algebra/Group/Action/TypeTags.lean b/Mathlib/Algebra/Group/Action/TypeTags.lean
index 0fa009b36d114..c6ceefe332560 100644
--- a/Mathlib/Algebra/Group/Action/TypeTags.lean
+++ b/Mathlib/Algebra/Group/Action/TypeTags.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Chris Hughes, Yury Kudryashov
 -/
 import Mathlib.Algebra.Group.Action.End
-import Mathlib.Algebra.Group.TypeTags
+import Mathlib.Algebra.Group.TypeTags.Hom
 
 /-!
 # Additive and Multiplicative for group actions
diff --git a/Mathlib/Algebra/Group/Equiv/TypeTags.lean b/Mathlib/Algebra/Group/Equiv/TypeTags.lean
index 78c085f074666..f8e14c0ceb128 100644
--- a/Mathlib/Algebra/Group/Equiv/TypeTags.lean
+++ b/Mathlib/Algebra/Group/Equiv/TypeTags.lean
@@ -5,7 +5,7 @@ Authors: Johannes Hölzl, Callum Sutton, Yury Kudryashov
 -/
 import Mathlib.Algebra.Group.Equiv.Basic
 import Mathlib.Algebra.Group.Prod
-import Mathlib.Algebra.Group.TypeTags
+import Mathlib.Algebra.Group.TypeTags.Hom
 
 /-!
 # Additive and multiplicative equivalences associated to `Multiplicative` and `Additive`.
diff --git a/Mathlib/Algebra/Group/Even.lean b/Mathlib/Algebra/Group/Even.lean
index 5bd24647c2f65..febd4c5c50c99 100644
--- a/Mathlib/Algebra/Group/Even.lean
+++ b/Mathlib/Algebra/Group/Even.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Damiano Testa
 -/
 import Mathlib.Algebra.Group.Opposite
-import Mathlib.Algebra.Group.TypeTags
+import Mathlib.Algebra.Group.TypeTags.Basic
 
 /-!
 # Squares and even elements
diff --git a/Mathlib/Algebra/Group/Subgroup/Map.lean b/Mathlib/Algebra/Group/Subgroup/Map.lean
index 84450e745384e..e1219dcd59203 100644
--- a/Mathlib/Algebra/Group/Subgroup/Map.lean
+++ b/Mathlib/Algebra/Group/Subgroup/Map.lean
@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Kexing Ying
 -/
 import Mathlib.Algebra.Group.Subgroup.Lattice
+import Mathlib.Algebra.Group.TypeTags.Hom
 
 /-!
 # `map` and `comap` for subgroups
diff --git a/Mathlib/Algebra/Group/Subsemigroup/Operations.lean b/Mathlib/Algebra/Group/Subsemigroup/Operations.lean
index 8fc45916faae0..2c782614c04cf 100644
--- a/Mathlib/Algebra/Group/Subsemigroup/Operations.lean
+++ b/Mathlib/Algebra/Group/Subsemigroup/Operations.lean
@@ -6,7 +6,7 @@ Amelia Livingston, Yury Kudryashov, Yakov Pechersky, Jireh Loreaux
 -/
 import Mathlib.Algebra.Group.Prod
 import Mathlib.Algebra.Group.Subsemigroup.Basic
-import Mathlib.Algebra.Group.TypeTags
+import Mathlib.Algebra.Group.TypeTags.Basic
 
 /-!
 # Operations on `Subsemigroup`s
diff --git a/Mathlib/Algebra/Group/TypeTags.lean b/Mathlib/Algebra/Group/TypeTags/Basic.lean
similarity index 80%
rename from Mathlib/Algebra/Group/TypeTags.lean
rename to Mathlib/Algebra/Group/TypeTags/Basic.lean
index f6e2f9c2cc9e0..c506dc1cf3541 100644
--- a/Mathlib/Algebra/Group/TypeTags.lean
+++ b/Mathlib/Algebra/Group/TypeTags/Basic.lean
@@ -3,8 +3,12 @@ Copyright (c) 2018 Mario Carneiro. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mario Carneiro
 -/
-import Mathlib.Algebra.Group.Hom.Defs
-import Mathlib.Data.Finite.Defs
+import Mathlib.Algebra.Group.Pi.Basic
+import Mathlib.Data.FunLike.Basic
+import Mathlib.Logic.Function.Iterate
+import Mathlib.Logic.Equiv.Defs
+import Mathlib.Tactic.Set
+import Mathlib.Util.AssertExists
 import Mathlib.Logic.Nontrivial.Basic
 
 /-!
@@ -32,6 +36,8 @@ This file is similar to `Order.Synonym`.
 
 assert_not_exists MonoidWithZero
 assert_not_exists DenselyOrdered
+assert_not_exists MonoidHom
+assert_not_exists Finite
 
 universe u v
 
@@ -136,16 +142,6 @@ instance [Inhabited α] : Inhabited (Multiplicative α) :=
 instance [Unique α] : Unique (Additive α) := toMul.unique
 instance [Unique α] : Unique (Multiplicative α) := toAdd.unique
 
-instance [Finite α] : Finite (Additive α) :=
-  Finite.of_equiv α (by rfl)
-
-instance [Finite α] : Finite (Multiplicative α) :=
-  Finite.of_equiv α (by rfl)
-
-instance [h : Infinite α] : Infinite (Additive α) := h
-
-instance [h : Infinite α] : Infinite (Multiplicative α) := h
-
 instance [h : DecidableEq α] : DecidableEq (Multiplicative α) := h
 
 instance [h : DecidableEq α] : DecidableEq (Additive α) := h
@@ -431,110 +427,6 @@ instance Additive.addCommGroup [CommGroup α] : AddCommGroup (Additive α) :=
 instance Multiplicative.commGroup [AddCommGroup α] : CommGroup (Multiplicative α) :=
   { Multiplicative.group, Multiplicative.commMonoid with }
 
-/-- Reinterpret `α →+ β` as `Multiplicative α →* Multiplicative β`. -/
-@[simps]
-def AddMonoidHom.toMultiplicative [AddZeroClass α] [AddZeroClass β] :
-    (α →+ β) ≃ (Multiplicative α →* Multiplicative β) where
-  toFun f := {
-    toFun := fun a => ofAdd (f (toAdd a))
-    map_mul' := f.map_add
-    map_one' := f.map_zero
-  }
-  invFun f := {
-    toFun := fun a => toAdd (f (ofAdd a))
-    map_add' := f.map_mul
-    map_zero' := f.map_one
-  }
-  left_inv _ := rfl
-  right_inv _ := rfl
-
-@[simp, norm_cast]
-lemma AddMonoidHom.coe_toMultiplicative [AddZeroClass α] [AddZeroClass β] (f : α →+ β) :
-    ⇑(toMultiplicative f) = ofAdd ∘ f ∘ toAdd := rfl
-
-/-- Reinterpret `α →* β` as `Additive α →+ Additive β`. -/
-@[simps]
-def MonoidHom.toAdditive [MulOneClass α] [MulOneClass β] :
-    (α →* β) ≃ (Additive α →+ Additive β) where
-  toFun f := {
-    toFun := fun a => ofMul (f (toMul a))
-    map_add' := f.map_mul
-    map_zero' := f.map_one
-  }
-  invFun f := {
-    toFun := fun a => toMul (f (ofMul a))
-    map_mul' := f.map_add
-    map_one' := f.map_zero
-  }
-  left_inv _ := rfl
-  right_inv _ := rfl
-
-@[simp, norm_cast]
-lemma MonoidHom.coe_toMultiplicative [MulOneClass α] [MulOneClass β] (f : α →* β) :
-    ⇑(toAdditive f) = ofMul ∘ f ∘ toMul := rfl
-
-/-- Reinterpret `Additive α →+ β` as `α →* Multiplicative β`. -/
-@[simps]
-def AddMonoidHom.toMultiplicative' [MulOneClass α] [AddZeroClass β] :
-    (Additive α →+ β) ≃ (α →* Multiplicative β) where
-  toFun f := {
-    toFun := fun a => ofAdd (f (ofMul a))
-    map_mul' := f.map_add
-    map_one' := f.map_zero
-  }
-  invFun f := {
-    toFun := fun a => toAdd (f (toMul a))
-    map_add' := f.map_mul
-    map_zero' := f.map_one
-  }
-  left_inv _ := rfl
-  right_inv _ := rfl
-
-@[simp, norm_cast]
-lemma AddMonoidHom.coe_toMultiplicative' [MulOneClass α] [AddZeroClass β] (f : Additive α →+ β) :
-    ⇑(toMultiplicative' f) = ofAdd ∘ f ∘ ofMul := rfl
-
-/-- Reinterpret `α →* Multiplicative β` as `Additive α →+ β`. -/
-@[simps!]
-def MonoidHom.toAdditive' [MulOneClass α] [AddZeroClass β] :
-    (α →* Multiplicative β) ≃ (Additive α →+ β) :=
-  AddMonoidHom.toMultiplicative'.symm
-
-@[simp, norm_cast]
-lemma MonoidHom.coe_toAdditive' [MulOneClass α] [AddZeroClass β] (f : α →* Multiplicative β) :
-    ⇑(toAdditive' f) = toAdd ∘ f ∘ toMul := rfl
-
-/-- Reinterpret `α →+ Additive β` as `Multiplicative α →* β`. -/
-@[simps]
-def AddMonoidHom.toMultiplicative'' [AddZeroClass α] [MulOneClass β] :
-    (α →+ Additive β) ≃ (Multiplicative α →* β) where
-  toFun f := {
-    toFun := fun a => toMul (f (toAdd a))
-    map_mul' := f.map_add
-    map_one' := f.map_zero
-  }
-  invFun f := {
-    toFun := fun a => ofMul (f (ofAdd a))
-    map_add' := f.map_mul
-    map_zero' := f.map_one
-  }
-  left_inv _ := rfl
-  right_inv _ := rfl
-
-@[simp, norm_cast]
-lemma AddMonoidHom.coe_toMultiplicative'' [AddZeroClass α] [MulOneClass β] (f : α →+ Additive β) :
-    ⇑(toMultiplicative'' f) = toMul ∘ f ∘ toAdd := rfl
-
-/-- Reinterpret `Multiplicative α →* β` as `α →+ Additive β`. -/
-@[simps!]
-def MonoidHom.toAdditive'' [AddZeroClass α] [MulOneClass β] :
-    (Multiplicative α →* β) ≃ (α →+ Additive β) :=
-  AddMonoidHom.toMultiplicative''.symm
-
-@[simp, norm_cast]
-lemma MonoidHom.coe_toAdditive'' [AddZeroClass α] [MulOneClass β] (f : Multiplicative α →* β) :
-    ⇑(toAdditive'' f) = ofMul ∘ f ∘ ofAdd := rfl
-
 /-- If `α` has some multiplicative structure and coerces to a function,
 then `Additive α` should also coerce to the same function.
 
diff --git a/Mathlib/Algebra/Group/TypeTags/Finite.lean b/Mathlib/Algebra/Group/TypeTags/Finite.lean
new file mode 100644
index 0000000000000..e3885696b373b
--- /dev/null
+++ b/Mathlib/Algebra/Group/TypeTags/Finite.lean
@@ -0,0 +1,28 @@
+/-
+Copyright (c) 2018 Mario Carneiro. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Mario Carneiro
+-/
+import Mathlib.Algebra.Group.TypeTags.Basic
+import Mathlib.Data.Finite.Defs
+
+/-!
+# `Finite` and `Infinite` are preserved by `Additive` and `Multiplicative`.
+-/
+
+assert_not_exists MonoidWithZero
+assert_not_exists DenselyOrdered
+
+universe u v
+
+variable {α : Type u}
+
+instance [Finite α] : Finite (Additive α) :=
+  Finite.of_equiv α (by rfl)
+
+instance [Finite α] : Finite (Multiplicative α) :=
+  Finite.of_equiv α (by rfl)
+
+instance [h : Infinite α] : Infinite (Additive α) := h
+
+instance [h : Infinite α] : Infinite (Multiplicative α) := h
diff --git a/Mathlib/Algebra/Group/TypeTags/Hom.lean b/Mathlib/Algebra/Group/TypeTags/Hom.lean
new file mode 100644
index 0000000000000..749c54aa7a8b7
--- /dev/null
+++ b/Mathlib/Algebra/Group/TypeTags/Hom.lean
@@ -0,0 +1,123 @@
+/-
+Copyright (c) 2018 Mario Carneiro. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Mario Carneiro
+-/
+import Mathlib.Algebra.Group.Hom.Defs
+import Mathlib.Algebra.Group.TypeTags.Basic
+
+/-!
+# Transport algebra morphisms between additive and multiplicative types.
+-/
+
+
+universe u v
+
+variable {α : Type u} {β : Type v}
+
+open Additive (ofMul toMul)
+open Multiplicative (ofAdd toAdd)
+
+/-- Reinterpret `α →+ β` as `Multiplicative α →* Multiplicative β`. -/
+@[simps]
+def AddMonoidHom.toMultiplicative [AddZeroClass α] [AddZeroClass β] :
+    (α →+ β) ≃ (Multiplicative α →* Multiplicative β) where
+  toFun f := {
+    toFun := fun a => ofAdd (f (toAdd a))
+    map_mul' := f.map_add
+    map_one' := f.map_zero
+  }
+  invFun f := {
+    toFun := fun a => toAdd (f (ofAdd a))
+    map_add' := f.map_mul
+    map_zero' := f.map_one
+  }
+  left_inv _ := rfl
+  right_inv _ := rfl
+
+@[simp, norm_cast]
+lemma AddMonoidHom.coe_toMultiplicative [AddZeroClass α] [AddZeroClass β] (f : α →+ β) :
+    ⇑(toMultiplicative f) = ofAdd ∘ f ∘ toAdd := rfl
+
+/-- Reinterpret `α →* β` as `Additive α →+ Additive β`. -/
+@[simps]
+def MonoidHom.toAdditive [MulOneClass α] [MulOneClass β] :
+    (α →* β) ≃ (Additive α →+ Additive β) where
+  toFun f := {
+    toFun := fun a => ofMul (f (toMul a))
+    map_add' := f.map_mul
+    map_zero' := f.map_one
+  }
+  invFun f := {
+    toFun := fun a => toMul (f (ofMul a))
+    map_mul' := f.map_add
+    map_one' := f.map_zero
+  }
+  left_inv _ := rfl
+  right_inv _ := rfl
+
+@[simp, norm_cast]
+lemma MonoidHom.coe_toMultiplicative [MulOneClass α] [MulOneClass β] (f : α →* β) :
+    ⇑(toAdditive f) = ofMul ∘ f ∘ toMul := rfl
+
+/-- Reinterpret `Additive α →+ β` as `α →* Multiplicative β`. -/
+@[simps]
+def AddMonoidHom.toMultiplicative' [MulOneClass α] [AddZeroClass β] :
+    (Additive α →+ β) ≃ (α →* Multiplicative β) where
+  toFun f := {
+    toFun := fun a => ofAdd (f (ofMul a))
+    map_mul' := f.map_add
+    map_one' := f.map_zero
+  }
+  invFun f := {
+    toFun := fun a => toAdd (f (toMul a))
+    map_add' := f.map_mul
+    map_zero' := f.map_one
+  }
+  left_inv _ := rfl
+  right_inv _ := rfl
+
+@[simp, norm_cast]
+lemma AddMonoidHom.coe_toMultiplicative' [MulOneClass α] [AddZeroClass β] (f : Additive α →+ β) :
+    ⇑(toMultiplicative' f) = ofAdd ∘ f ∘ ofMul := rfl
+
+/-- Reinterpret `α →* Multiplicative β` as `Additive α →+ β`. -/
+@[simps!]
+def MonoidHom.toAdditive' [MulOneClass α] [AddZeroClass β] :
+    (α →* Multiplicative β) ≃ (Additive α →+ β) :=
+  AddMonoidHom.toMultiplicative'.symm
+
+@[simp, norm_cast]
+lemma MonoidHom.coe_toAdditive' [MulOneClass α] [AddZeroClass β] (f : α →* Multiplicative β) :
+    ⇑(toAdditive' f) = toAdd ∘ f ∘ toMul := rfl
+
+/-- Reinterpret `α →+ Additive β` as `Multiplicative α →* β`. -/
+@[simps]
+def AddMonoidHom.toMultiplicative'' [AddZeroClass α] [MulOneClass β] :
+    (α →+ Additive β) ≃ (Multiplicative α →* β) where
+  toFun f := {
+    toFun := fun a => toMul (f (toAdd a))
+    map_mul' := f.map_add
+    map_one' := f.map_zero
+  }
+  invFun f := {
+    toFun := fun a => ofMul (f (ofAdd a))
+    map_add' := f.map_mul
+    map_zero' := f.map_one
+  }
+  left_inv _ := rfl
+  right_inv _ := rfl
+
+@[simp, norm_cast]
+lemma AddMonoidHom.coe_toMultiplicative'' [AddZeroClass α] [MulOneClass β] (f : α →+ Additive β) :
+    ⇑(toMultiplicative'' f) = toMul ∘ f ∘ toAdd := rfl
+
+/-- Reinterpret `Multiplicative α →* β` as `α →+ Additive β`. -/
+@[simps!]
+def MonoidHom.toAdditive'' [AddZeroClass α] [MulOneClass β] :
+    (Multiplicative α →* β) ≃ (α →+ Additive β) :=
+  AddMonoidHom.toMultiplicative''.symm
+
+@[simp, norm_cast]
+lemma MonoidHom.coe_toAdditive'' [AddZeroClass α] [MulOneClass β] (f : Multiplicative α →* β) :
+    ⇑(toAdditive'' f) = ofMul ∘ f ∘ ofAdd := rfl
diff --git a/Mathlib/Algebra/Order/Monoid/Unbundled/TypeTags.lean b/Mathlib/Algebra/Order/Monoid/Unbundled/TypeTags.lean
index 1647d43c6a434..a975f6b4f3384 100644
--- a/Mathlib/Algebra/Order/Monoid/Unbundled/TypeTags.lean
+++ b/Mathlib/Algebra/Order/Monoid/Unbundled/TypeTags.lean
@@ -3,9 +3,9 @@ Copyright (c) 2016 Jeremy Avigad. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Jeremy Avigad, Leonardo de Moura, Mario Carneiro, Johannes Hölzl
 -/
-import Mathlib.Algebra.Group.TypeTags
 import Mathlib.Algebra.Order.Monoid.Unbundled.ExistsOfLE
 import Mathlib.Order.BoundedOrder
+import Mathlib.Algebra.Group.TypeTags.Basic
 
 /-! # Ordered monoid structures on `Multiplicative α` and `Additive α`. -/
 
diff --git a/Mathlib/Analysis/Normed/Field/Lemmas.lean b/Mathlib/Analysis/Normed/Field/Lemmas.lean
index e22f72874193c..88affc76dbe77 100644
--- a/Mathlib/Analysis/Normed/Field/Lemmas.lean
+++ b/Mathlib/Analysis/Normed/Field/Lemmas.lean
@@ -5,6 +5,7 @@ Authors: Patrick Massot, Johannes Hölzl
 -/
 
 import Mathlib.Algebra.Group.AddChar
+import Mathlib.Algebra.Group.TypeTags.Finite
 import Mathlib.Algebra.Order.Ring.Finset
 import Mathlib.Analysis.Normed.Field.Basic
 import Mathlib.Analysis.Normed.Group.Bounded
diff --git a/Mathlib/Data/Finsupp/Defs.lean b/Mathlib/Data/Finsupp/Defs.lean
index 7ac40e922fd7b..be9894c31daf0 100644
--- a/Mathlib/Data/Finsupp/Defs.lean
+++ b/Mathlib/Data/Finsupp/Defs.lean
@@ -7,6 +7,7 @@ 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
 
 /-!
 # Type of functions with finite support
diff --git a/Mathlib/Data/Fintype/Basic.lean b/Mathlib/Data/Fintype/Basic.lean
index 3bda18e430ecb..d77529bf9ac3e 100644
--- a/Mathlib/Data/Fintype/Basic.lean
+++ b/Mathlib/Data/Fintype/Basic.lean
@@ -5,6 +5,7 @@ Authors: Mario Carneiro
 -/
 import Mathlib.Data.Finset.Image
 import Mathlib.Data.List.FinRange
+import Mathlib.Data.Finite.Defs
 
 /-!
 # Finite types
diff --git a/Mathlib/Data/Nat/Cast/Basic.lean b/Mathlib/Data/Nat/Cast/Basic.lean
index d4f2aa9e4fd08..b8cda137de314 100644
--- a/Mathlib/Data/Nat/Cast/Basic.lean
+++ b/Mathlib/Data/Nat/Cast/Basic.lean
@@ -6,6 +6,7 @@ Authors: Mario Carneiro
 import Mathlib.Algebra.Divisibility.Basic
 import Mathlib.Algebra.Ring.Hom.Defs
 import Mathlib.Algebra.Ring.Nat
+import Mathlib.Algebra.Group.TypeTags.Hom
 
 /-!
 # Cast of natural numbers (additional theorems)
diff --git a/Mathlib/Deprecated/Group.lean b/Mathlib/Deprecated/Group.lean
index 539782f49e725..66bc94fe1317e 100644
--- a/Mathlib/Deprecated/Group.lean
+++ b/Mathlib/Deprecated/Group.lean
@@ -4,9 +4,9 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yury Kudryashov
 -/
 import Mathlib.Algebra.Group.Equiv.Basic
-import Mathlib.Algebra.Group.TypeTags
 import Mathlib.Algebra.Group.Units.Hom
 import Mathlib.Algebra.Ring.Hom.Defs
+import Mathlib.Algebra.Group.TypeTags.Basic
 
 /-!
 # Unbundled monoid and group homomorphisms
diff --git a/Mathlib/GroupTheory/FiniteAbelian/Basic.lean b/Mathlib/GroupTheory/FiniteAbelian/Basic.lean
index def95dc958b3b..38fa544799b25 100644
--- a/Mathlib/GroupTheory/FiniteAbelian/Basic.lean
+++ b/Mathlib/GroupTheory/FiniteAbelian/Basic.lean
@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Pierre-Alexandre Bazin
 -/
 import Mathlib.Algebra.Module.PID
+import Mathlib.Algebra.Group.TypeTags.Finite
 import Mathlib.Data.ZMod.Quotient
 
 /-!