chore(Data/Nat/Cast): don't import MonoidWithZero for results about…

… `MonoidHom` (#20745)

For this, move the results from `Data.Nat.Cast.Basic` not mentioning `Nat.cast` (!) to a new file `Algebra.Group.Nat.Hom`.

See leanprover-community/mathlib3#2957 for the copyright attribution.

Mathlib.lean

@@ -311,6 +311,7 @@ import Mathlib.Algebra.Group.Invertible.Defs
 import Mathlib.Algebra.Group.MinimalAxioms
 import Mathlib.Algebra.Group.Nat.Defs
 import Mathlib.Algebra.Group.Nat.Even
+import Mathlib.Algebra.Group.Nat.Hom
 import Mathlib.Algebra.Group.Nat.TypeTags
 import Mathlib.Algebra.Group.Nat.Units
 import Mathlib.Algebra.Group.NatPowAssoc

Mathlib/Algebra/Category/MonCat/ForgetCorepresentable.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Sophie Morel
 -/
 import Mathlib.Algebra.Category.MonCat.Basic
-import Mathlib.Data.Nat.Cast.Basic
+import Mathlib.Algebra.Group.Nat.Hom
 
 /-!
 # The forget functor is corepresentable

Mathlib/Algebra/Group/Nat/Hom.lean

@@ -0,0 +1,125 @@
+/-
+Copyright (c) 2020 Yury Kudryashov. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Yury Kudryashov
+-/
+import Mathlib.Algebra.Group.Equiv.Defs
+import Mathlib.Algebra.Group.Hom.Basic
+import Mathlib.Algebra.Group.Nat.Defs
+import Mathlib.Algebra.Group.TypeTags.Hom
+import Mathlib.Tactic.MinImports
+
+/-!
+# Extensionality of monoid homs from `ℕ`
+-/
+
+assert_not_exists OrderedCommMonoid MonoidWithZero
+
+open Additive Multiplicative
+
+variable {M M : Type*}
+
+section AddMonoidHomClass
+
+variable {A B F : Type*} [FunLike F ℕ A]
+
+lemma ext_nat' [AddMonoid A] [AddMonoidHomClass F ℕ A] (f g : F) (h : f 1 = g 1) : f = g :=
+  DFunLike.ext f g <| by
+    intro n
+    induction n with
+    | zero => simp_rw [map_zero f, map_zero g]
+    | succ n ihn =>
+      simp [h, ihn]
+
+@[ext]
+lemma AddMonoidHom.ext_nat [AddMonoid A] {f g : ℕ →+ A} : f 1 = g 1 → f = g :=
+  ext_nat' f g
+
+end AddMonoidHomClass
+
+section AddMonoid
+variable [AddMonoid M]
+
+variable (M) in
+/-- Additive homomorphisms from `ℕ` are defined by the image of `1`. -/
+def multiplesHom : M ≃ (ℕ →+ M) where
+  toFun x :=
+  { toFun := fun n ↦ n • x
+    map_zero' := zero_nsmul x
+    map_add' := fun _ _ ↦ add_nsmul _ _ _ }
+  invFun f := f 1
+  left_inv := one_nsmul
+  right_inv f := AddMonoidHom.ext_nat <| one_nsmul (f 1)
+
+@[simp] lemma multiplesHom_apply (x : M) (n : ℕ) : multiplesHom M x n = n • x := rfl
+
+lemma multiplesHom_symm_apply (f : ℕ →+ M) : (multiplesHom M).symm f = f 1 := rfl
+
+lemma AddMonoidHom.apply_nat (f : ℕ →+ M) (n : ℕ) : f n = n • f 1 := by
+  rw [← multiplesHom_symm_apply, ← multiplesHom_apply, Equiv.apply_symm_apply]
+
+end AddMonoid
+
+section Monoid
+variable [Monoid M]
+
+variable (M) in
+/-- Monoid homomorphisms from `Multiplicative ℕ` are defined by the image
+of `Multiplicative.ofAdd 1`. -/
+@[to_additive existing]
+def powersHom : M ≃ (Multiplicative ℕ →* M) :=
+  Additive.ofMul.trans <| (multiplesHom _).trans <| AddMonoidHom.toMultiplicative''
+
+@[to_additive existing (attr := simp)]
+lemma powersHom_apply (x : M) (n : Multiplicative ℕ) :
+    powersHom M x n = x ^ n.toAdd := rfl
+
+@[to_additive existing (attr := simp)]
+lemma powersHom_symm_apply (f : Multiplicative ℕ →* M) :
+    (powersHom M).symm f = f (Multiplicative.ofAdd 1) := rfl
+
+@[to_additive existing AddMonoidHom.apply_nat]
+lemma MonoidHom.apply_mnat (f : Multiplicative ℕ →* M) (n : Multiplicative ℕ) :
+    f n = f (Multiplicative.ofAdd 1) ^ n.toAdd := by
+  rw [← powersHom_symm_apply, ← powersHom_apply, Equiv.apply_symm_apply]
+
+@[to_additive existing (attr := ext) AddMonoidHom.ext_nat]
+lemma MonoidHom.ext_mnat ⦃f g : Multiplicative ℕ →* M⦄
+    (h : f (Multiplicative.ofAdd 1) = g (Multiplicative.ofAdd 1)) : f = g :=
+  MonoidHom.ext fun n ↦ by rw [f.apply_mnat, g.apply_mnat, h]
+
+end Monoid
+
+section AddCommMonoid
+variable [AddCommMonoid M]
+
+variable (M) in
+/-- If `M` is commutative, `multiplesHom` is an additive equivalence. -/
+def multiplesAddHom : M ≃+ (ℕ →+ M) where
+  __ := multiplesHom M
+  map_add' a b := AddMonoidHom.ext fun n ↦ by simp [nsmul_add]
+
+@[simp] lemma multiplesAddHom_apply (x : M) (n : ℕ) : multiplesAddHom M x n = n • x := rfl
+
+@[simp] lemma multiplesAddHom_symm_apply (f : ℕ →+ M) : (multiplesAddHom M).symm f = f 1 := rfl
+
+end AddCommMonoid
+
+section CommMonoid
+variable [CommMonoid M]
+
+variable (M) in
+/-- If `M` is commutative, `powersHom` is a multiplicative equivalence. -/
+@[to_additive existing]
+def powersMulHom : M ≃* (Multiplicative ℕ →* M) where
+  __ := powersHom M
+  map_mul' a b := MonoidHom.ext fun n ↦ by simp [mul_pow]
+
+@[to_additive existing (attr := simp)]
+lemma powersMulHom_apply (x : M) (n : Multiplicative ℕ) : powersMulHom M x n = x ^ n.toAdd := rfl
+
+@[to_additive existing (attr := simp)]
+lemma powersMulHom_symm_apply (f : Multiplicative ℕ →* M) : (powersMulHom M).symm f = f (ofAdd 1) :=
+  rfl
+
+end CommMonoid

Mathlib/Algebra/Group/Submonoid/Membership.lean

@@ -6,6 +6,7 @@ Amelia Livingston, Yury Kudryashov
 -/
 import Mathlib.Algebra.FreeMonoid.Basic
 import Mathlib.Algebra.Group.Idempotent
+import Mathlib.Algebra.Group.Nat.Hom
 import Mathlib.Algebra.Group.Submonoid.MulOpposite
 import Mathlib.Algebra.Group.Submonoid.Operations
 import Mathlib.Algebra.GroupWithZero.Divisibility

Mathlib/Algebra/Polynomial/Eval/Defs.lean

@@ -3,6 +3,7 @@ Copyright (c) 2018 Chris Hughes. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Chris Hughes, Johannes Hölzl, Kim Morrison, Jens Wagemaker
 -/
+import Mathlib.Algebra.Group.Nat.Hom
 import Mathlib.Algebra.Polynomial.Basic
 
 /-!

Mathlib/Algebra/Polynomial/Monomial.lean

@@ -3,12 +3,11 @@ Copyright (c) 2018 Chris Hughes. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Chris Hughes, Johannes Hölzl, Kim Morrison, Jens Wagemaker
 -/
+import Mathlib.Algebra.Group.Nat.Hom
 import Mathlib.Algebra.Polynomial.Basic
 
 /-!
 # Univariate monomials
-
-Preparatory lemmas for degree_basic.
 -/
 
 

Mathlib/Data/Int/Cast/Lemmas.lean

@@ -3,6 +3,7 @@ Copyright (c) 2017 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.Hom
 import Mathlib.Algebra.Ring.Hom.Basic
 import Mathlib.Algebra.Ring.Int.Defs
 import Mathlib.Algebra.Ring.Parity

Mathlib/Data/Nat/Cast/Basic.lean

@@ -5,7 +5,7 @@ Authors: Mario Carneiro
 -/
 import Mathlib.Algebra.Divisibility.Hom
 import Mathlib.Algebra.Group.Even
-import Mathlib.Algebra.Group.TypeTags.Hom
+import Mathlib.Algebra.Group.Nat.Hom
 import Mathlib.Algebra.Ring.Hom.Defs
 import Mathlib.Algebra.Ring.Nat
 
@@ -92,21 +92,7 @@ end Nat
 
 section AddMonoidHomClass
 
-variable {A B F : Type*} [AddMonoidWithOne B] [FunLike F ℕ A]
-
-theorem ext_nat' [AddMonoid A] [AddMonoidHomClass F ℕ A] (f g : F) (h : f 1 = g 1) : f = g :=
-  DFunLike.ext f g <| by
-    intro n
-    induction n with
-    | zero => simp_rw [map_zero f, map_zero g]
-    | succ n ihn =>
-      simp [h, ihn]
-
-@[ext]
-theorem AddMonoidHom.ext_nat [AddMonoid A] {f g : ℕ →+ A} : f 1 = g 1 → f = g :=
-  ext_nat' f g
-
-variable [AddMonoidWithOne A]
+variable {A B F : Type*} [AddMonoidWithOne B] [FunLike F ℕ A] [AddMonoidWithOne A]
 
 -- these versions are primed so that the `RingHomClass` versions aren't
 theorem eq_natCast' [AddMonoidHomClass F ℕ A] (f : F) (h1 : f 1 = 1) : ∀ n : ℕ, f n = n
@@ -195,78 +181,6 @@ instance Nat.uniqueRingHom {R : Type*} [NonAssocSemiring R] : Unique (ℕ →+*
   default := Nat.castRingHom R
   uniq := RingHom.eq_natCast'
 
-section Monoid
-variable (α) [Monoid α] (β) [AddMonoid β]
-
-/-- Additive homomorphisms from `ℕ` are defined by the image of `1`. -/
-def multiplesHom : β ≃ (ℕ →+ β) where
-  toFun x :=
-  { toFun := fun n ↦ n • x
-    map_zero' := zero_nsmul x
-    map_add' := fun _ _ ↦ add_nsmul _ _ _ }
-  invFun f := f 1
-  left_inv := one_nsmul
-  right_inv f := AddMonoidHom.ext_nat <| one_nsmul (f 1)
-
-/-- Monoid homomorphisms from `Multiplicative ℕ` are defined by the image
-of `Multiplicative.ofAdd 1`. -/
-@[to_additive existing]
-def powersHom : α ≃ (Multiplicative ℕ →* α) :=
-  Additive.ofMul.trans <| (multiplesHom _).trans <| AddMonoidHom.toMultiplicative''
-
-variable {α}
-
--- TODO: can `to_additive` generate the following lemmas automatically?
-
-lemma multiplesHom_apply (x : β) (n : ℕ) : multiplesHom β x n = n • x := rfl
-
-@[to_additive existing (attr := simp)]
-lemma powersHom_apply (x : α) (n : Multiplicative ℕ) :
-    powersHom α x n = x ^ n.toAdd := rfl
-
-lemma multiplesHom_symm_apply (f : ℕ →+ β) : (multiplesHom β).symm f = f 1 := rfl
-
-@[to_additive existing (attr := simp)]
-lemma powersHom_symm_apply (f : Multiplicative ℕ →* α) :
-    (powersHom α).symm f = f (Multiplicative.ofAdd 1) := rfl
-
-lemma MonoidHom.apply_mnat (f : Multiplicative ℕ →* α) (n : Multiplicative ℕ) :
-    f n = f (Multiplicative.ofAdd 1) ^ n.toAdd := by
-  rw [← powersHom_symm_apply, ← powersHom_apply, Equiv.apply_symm_apply]
-
-@[ext]
-lemma MonoidHom.ext_mnat ⦃f g : Multiplicative ℕ →* α⦄
-    (h : f (Multiplicative.ofAdd 1) = g (Multiplicative.ofAdd 1)) : f = g :=
-  MonoidHom.ext fun n ↦ by rw [f.apply_mnat, g.apply_mnat, h]
-
-lemma AddMonoidHom.apply_nat (f : ℕ →+ β) (n : ℕ) : f n = n • f 1 := by
-  rw [← multiplesHom_symm_apply, ← multiplesHom_apply, Equiv.apply_symm_apply]
-
-end Monoid
-
-section CommMonoid
-variable (α) [CommMonoid α] (β) [AddCommMonoid β]
-
-/-- If `α` is commutative, `multiplesHom` is an additive equivalence. -/
-def multiplesAddHom : β ≃+ (ℕ →+ β) :=
-  { multiplesHom β with map_add' := fun a b ↦ AddMonoidHom.ext fun n ↦ by simp [nsmul_add] }
-
-/-- If `α` is commutative, `powersHom` is a multiplicative equivalence. -/
-def powersMulHom : α ≃* (Multiplicative ℕ →* α) :=
-  { powersHom α with map_mul' := fun a b ↦ MonoidHom.ext fun n ↦ by simp [mul_pow] }
-
-@[simp] lemma multiplesAddHom_apply (x : β) (n : ℕ) : multiplesAddHom β x n = n • x := rfl
-
-@[simp]
-lemma powersMulHom_apply (x : α) (n : Multiplicative ℕ) : powersMulHom α x n = x ^ n.toAdd := rfl
-
-@[simp] lemma multiplesAddHom_symm_apply (f : ℕ →+ β) : (multiplesAddHom β).symm f = f 1 := rfl
-
-@[simp] lemma powersMulHom_symm_apply (f : Multiplicative ℕ →* α) :
-    (powersMulHom α).symm f = f (ofAdd 1) := rfl
-
-end CommMonoid
-
 namespace Pi
 
 variable {π : α → Type*} [∀ a, NatCast (π a)]