chore: split Algebra.Group.TypeTags (#19351)

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

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
 
 /-!

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

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

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`.

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

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

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

Mathlib/Algebra/Group/TypeTags.lean → 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.
 

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

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

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 α`. -/
 

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