feat: generalize Mathlib.Algebra.Group+Ring+Field (#23143)

This is one of a series of PRs that generalizes type classes across Mathlib. These are generated using a new linter that tries to re-elaborate theorem definitions with more general type classes to see if it succeeds. It will accept the generalization if deleting the entire type class causes the theorem to fail to compile, and the old type class can not simply be re-synthesized with the new declaration. Otherwise, the generalization is rejected as the type class is not being generalized, but can simply be replaced by implicit type class synthesis or an implicit type class in a variable block being pulled in.

The linter currently output debug statements indicating source file positions where type classes should be generalized, and a script then makes those edits. This file contains a subset of those generalizations. The linter and the script performing re-writes is available in commit 5e2b704.

Also see discussion on Zulip here:
https://leanprover.zulipchat.com/#narrow/channel/270676-lean4/topic/Elab.20to.20generalize.20type.20classes.20for.20theorems/near/498862988 https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Elab.20to.20generalize.20type.20classes.20for.20theorems/near/501288855

Author: vlad902

Mathlib/Algebra/Field/NegOnePow.lean

@@ -11,7 +11,7 @@ import Mathlib.Tactic.NormNum
 
 namespace Int
 
-lemma cast_negOnePow (K : Type*) (n : ℤ) [Field K] : n.negOnePow = (-1 : K) ^ n := by
+lemma cast_negOnePow (K : Type*) (n : ℤ) [DivisionRing K] : n.negOnePow = (-1 : K) ^ n := by
   rcases even_or_odd' n with ⟨k, rfl | rfl⟩
   · simp [zpow_mul, zpow_ofNat]
   · rw [zpow_add_one₀ (by norm_num), zpow_mul, zpow_ofNat]

Mathlib/Algebra/Field/Periodic.lean

@@ -111,30 +111,30 @@ theorem Periodic.image_uIcc [LinearOrderedAddCommGroup α] [Archimedean α] (h :
 
 /-! ### Antiperiodicity -/
 
-theorem Antiperiodic.add_nat_mul_eq [Semiring α] [Ring β] (h : Antiperiodic f c) (n : ℕ) :
+theorem Antiperiodic.add_nat_mul_eq [NonAssocSemiring α] [Ring β] (h : Antiperiodic f c) (n : ℕ) :
     f (x + n * c) = (-1) ^ n * f x := by
   simpa only [nsmul_eq_mul, zsmul_eq_mul, Int.cast_pow, Int.cast_neg,
     Int.cast_one] using h.add_nsmul_eq n
 
-theorem Antiperiodic.sub_nat_mul_eq [Ring α] [Ring β] (h : Antiperiodic f c) (n : ℕ) :
+theorem Antiperiodic.sub_nat_mul_eq [NonAssocRing α] [Ring β] (h : Antiperiodic f c) (n : ℕ) :
     f (x - n * c) = (-1) ^ n * f x := by
   simpa only [nsmul_eq_mul, zsmul_eq_mul, Int.cast_pow, Int.cast_neg,
     Int.cast_one] using h.sub_nsmul_eq n
 
-theorem Antiperiodic.nat_mul_sub_eq [Ring α] [Ring β] (h : Antiperiodic f c) (n : ℕ) :
+theorem Antiperiodic.nat_mul_sub_eq [NonAssocRing α] [Ring β] (h : Antiperiodic f c) (n : ℕ) :
     f (n * c - x) = (-1) ^ n * f (-x) := by
   simpa only [nsmul_eq_mul, zsmul_eq_mul, Int.cast_pow, Int.cast_neg,
     Int.cast_one] using h.nsmul_sub_eq n
 
-theorem Antiperiodic.const_smul₀ [AddCommMonoid α] [Neg β] [DivisionSemiring γ] [Module γ α]
+theorem Antiperiodic.const_smul₀ [AddMonoid α] [Neg β] [GroupWithZero γ] [DistribMulAction γ α]
     (h : Antiperiodic f c) {a : γ} (ha : a ≠ 0) : Antiperiodic (fun x => f (a • x)) (a⁻¹ • c) :=
   fun x => by simpa only [smul_add, smul_inv_smul₀ ha] using h (a • x)
 
 theorem Antiperiodic.const_mul [DivisionSemiring α] [Neg β] (h : Antiperiodic f c) {a : α}
     (ha : a ≠ 0) : Antiperiodic (fun x => f (a * x)) (a⁻¹ * c) :=
   h.const_smul₀ ha
 
-theorem Antiperiodic.const_inv_smul₀ [AddCommMonoid α] [Neg β] [DivisionSemiring γ] [Module γ α]
+theorem Antiperiodic.const_inv_smul₀ [AddMonoid α] [Neg β] [GroupWithZero γ] [DistribMulAction γ α]
     (h : Antiperiodic f c) {a : γ} (ha : a ≠ 0) : Antiperiodic (fun x => f (a⁻¹ • x)) (a • c) := by
   simpa only [inv_inv] using h.const_smul₀ (inv_ne_zero ha)
 

Mathlib/Algebra/Group/Action/Pointwise/Finset.lean

@@ -146,8 +146,8 @@ theorem pairwiseDisjoint_smul_iff {s : Set α} {t : Finset α} :
 end IsLeftCancelMul
 
 @[to_additive]
-theorem image_smul_distrib [DecidableEq α] [DecidableEq β] [Monoid α] [Monoid β] [FunLike F α β]
-    [MonoidHomClass F α β] (f : F) (a : α) (s : Finset α) : (a • s).image f = f a • s.image f :=
+theorem image_smul_distrib [DecidableEq α] [DecidableEq β] [Mul α] [Mul β] [FunLike F α β]
+    [MulHomClass F α β] (f : F) (a : α) (s : Finset α) : (a • s).image f = f a • s.image f :=
   image_comm <| map_mul _ _
 
 section Group

Mathlib/Algebra/Group/Action/Pointwise/Set/Basic.lean

@@ -92,14 +92,14 @@ open scoped RightActions
 end Mul
 
 @[to_additive]
-lemma image_smul_distrib [MulOneClass α] [MulOneClass β] [FunLike F α β] [MonoidHomClass F α β]
+lemma image_smul_distrib [Mul α] [Mul β] [FunLike F α β] [MulHomClass F α β]
     (f : F) (a : α) (s : Set α) :
     f '' (a • s) = f a • f '' s :=
   image_comm <| map_mul _ _
 
 open scoped RightActions in
 @[to_additive]
-lemma image_op_smul_distrib [MulOneClass α] [MulOneClass β] [FunLike F α β] [MonoidHomClass F α β]
+lemma image_op_smul_distrib [Mul α] [Mul β] [FunLike F α β] [MulHomClass F α β]
     (f : F) (a : α) (s : Set α) : f '' (s <• a) = f '' s <• f a := image_comm fun _ ↦ map_mul ..
 
 section Semigroup

Mathlib/Algebra/Group/Defs.lean

@@ -457,7 +457,7 @@ def nsmulRec' {M : Type*} [Zero M] [Add M] : ℕ → M → M
 attribute [to_additive existing] npowRec'
 
 @[to_additive]
-theorem npowRec'_succ {M : Type*} [Semigroup M] [One M] {k : ℕ} (_ : k ≠ 0) (m : M) :
+theorem npowRec'_succ {M : Type*} [Mul M] [One M] {k : ℕ} (_ : k ≠ 0) (m : M) :
     npowRec' (k + 1) m = npowRec' k m * m :=
   match k with
   | _ + 1 => rfl

Mathlib/Algebra/Group/Embedding.lean

@@ -35,7 +35,7 @@ def mulRightEmbedding [Mul G] [IsRightCancelMul G] (g : G) : G ↪ G where
   inj' := mul_left_injective g
 
 @[to_additive]
-theorem mulLeftEmbedding_eq_mulRightEmbedding [CommSemigroup G] [IsCancelMul G] (g : G) :
+theorem mulLeftEmbedding_eq_mulRightEmbedding [CommMagma G] [IsCancelMul G] (g : G) :
     mulLeftEmbedding g = mulRightEmbedding g := by
   ext
   exact mul_comm _ _

Mathlib/Algebra/Group/ForwardDiff.lean

@@ -57,7 +57,7 @@ lemma fwdDiff_smul {R : Type} [Ring R] [Module R G] (f : M → R) (g : M → G)
 
 -- Note `fwdDiff_const_smul` is more general than `fwdDiff_smul` since it allows `R` to be a
 -- semiring, rather than a ring; in particular `R = ℕ` is allowed.
-@[simp] lemma fwdDiff_const_smul {R : Type*} [Semiring R] [Module R G] (r : R) (f : M → G) :
+@[simp] lemma fwdDiff_const_smul {R : Type*} [Monoid R] [DistribMulAction R G] (r : R) (f : M → G) :
     Δ_[h] (r • f) = r • Δ_[h] f :=
   funext fun _ ↦ (smul_sub ..).symm
 
@@ -118,7 +118,7 @@ open fwdDiff_aux
     Δ_[h]^[n] (f + g) = Δ_[h]^[n] f + Δ_[h]^[n] g := by
   simpa only [coe_fwdDiffₗ_pow] using map_add (fwdDiffₗ M G h ^ n) f g
 
-@[simp] lemma fwdDiff_iter_const_smul {R : Type*} [Semiring R] [Module R G]
+@[simp] lemma fwdDiff_iter_const_smul {R : Type*} [Monoid R] [DistribMulAction R G]
     (r : R) (f : M → G) (n : ℕ) : Δ_[h]^[n] (r • f) = r • Δ_[h]^[n] f := by
   induction' n with n IH generalizing f
   · simp only [iterate_zero, id_eq]

Mathlib/Algebra/Group/Hom/Defs.lean

@@ -414,7 +414,7 @@ theorem map_div' [DivInvMonoid G] [DivInvMonoid H] [MulHomClass F G H]
   rw [div_eq_mul_inv, div_eq_mul_inv, map_mul, hf]
 
 @[to_additive]
-lemma map_comp_div' [DivInvMonoid G] [DivInvMonoid H] [MonoidHomClass F G H] (f : F)
+lemma map_comp_div' [DivInvMonoid G] [DivInvMonoid H] [MulHomClass F G H] (f : F)
     (hf : ∀ a, f a⁻¹ = (f a)⁻¹) (g h : ι → G) : f ∘ (g / h) = f ∘ g / f ∘ h := by
   ext; simp [map_div' f hf]
 

Mathlib/Algebra/Group/Hom/Instances.lean

@@ -78,7 +78,7 @@ theorem AddMonoid.End.zero_apply [AddCommMonoid M] (m : M) : (0 : AddMonoid.End
   rfl
 
 -- Note: `@[simp]` omitted because `(1 : AddMonoid.End M) = id` by `AddMonoid.End.coe_one`
-theorem AddMonoid.End.one_apply [AddCommMonoid M] (m : M) : (1 : AddMonoid.End M) m = m :=
+theorem AddMonoid.End.one_apply [AddZeroClass M] (m : M) : (1 : AddMonoid.End M) m = m :=
   rfl
 
 instance AddMonoid.End.instAddCommGroup [AddCommGroup M] : AddCommGroup (AddMonoid.End M) :=

Mathlib/Algebra/Group/Nat/Hom.lean

@@ -23,7 +23,7 @@ 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 :=
+lemma ext_nat' [AddZeroClass A] [AddMonoidHomClass F ℕ A] (f g : F) (h : f 1 = g 1) : f = g :=
   DFunLike.ext f g <| by
     intro n
     induction n with
@@ -32,7 +32,7 @@ lemma ext_nat' [AddMonoid A] [AddMonoidHomClass F ℕ A] (f g : F) (h : f 1 = g
       simp [h, ihn]
 
 @[ext]
-lemma AddMonoidHom.ext_nat [AddMonoid A] {f g : ℕ →+ A} : f 1 = g 1 → f = g :=
+lemma AddMonoidHom.ext_nat [AddZeroClass A] {f g : ℕ →+ A} : f 1 = g 1 → f = g :=
   ext_nat' f g
 
 end AddMonoidHomClass

Mathlib/Algebra/Group/Pointwise/Set/Basic.lean

@@ -1257,13 +1257,13 @@ lemma MapsTo.mul [Mul β] {A : Set α} {B₁ B₂ : Set β} {f₁ f₂ : α →
   fun _ h => mul_mem_mul (h₁ h) (h₂ h)
 
 @[to_additive]
-lemma MapsTo.inv [DivisionCommMonoid β] {A : Set α} {B : Set β} {f : α → β} (h : MapsTo f A B) :
+lemma MapsTo.inv [InvolutiveInv β] {A : Set α} {B : Set β} {f : α → β} (h : MapsTo f A B) :
     MapsTo (f⁻¹) A (B⁻¹) :=
   fun _ ha => inv_mem_inv.2 (h ha)
 
 
 @[to_additive]
-lemma MapsTo.div [DivisionCommMonoid β] {A : Set α} {B₁ B₂ : Set β} {f₁ f₂ : α → β}
+lemma MapsTo.div [Div β] {A : Set α} {B₁ B₂ : Set β} {f₁ f₂ : α → β}
     (h₁ : MapsTo f₁ A B₁) (h₂ : MapsTo f₂ A B₂) : MapsTo (f₁ / f₂) A (B₁ / B₂) :=
   fun _ ha => div_mem_div (h₁ ha) (h₂ ha)
 

Mathlib/Algebra/Group/Pointwise/Set/BigOperators.lean

@@ -104,7 +104,7 @@ theorem list_prod_subset_list_prod (t : List ι) (f₁ f₂ : ι → Set α) (hf
       (ih fun i hi ↦ hf i <| List.mem_cons_of_mem _ hi)
 
 @[to_additive]
-theorem list_prod_singleton {M : Type*} [CommMonoid M] (s : List M) :
+theorem list_prod_singleton {M : Type*} [Monoid M] (s : List M) :
     (s.map fun i ↦ ({i} : Set M)).prod = {s.prod} :=
   (map_list_prod (singletonMonoidHom : M →* Set M) _).symm
 

Mathlib/Algebra/Group/Subgroup/Ker.lean

@@ -320,7 +320,7 @@ theorem coe_toAdditive_ker (f : G →* G') :
     (MonoidHom.toAdditive f).ker = Subgroup.toAddSubgroup f.ker := rfl
 
 @[simp]
-theorem coe_toMultiplicative_ker {A A' : Type*} [AddGroup A] [AddGroup A'] (f : A →+ A') :
+theorem coe_toMultiplicative_ker {A A' : Type*} [AddGroup A] [AddZeroClass A'] (f : A →+ A') :
     (AddMonoidHom.toMultiplicative f).ker = AddSubgroup.toSubgroup f.ker := rfl
 
 end Ker

Mathlib/Algebra/Group/Subgroup/Order.lean

@@ -123,6 +123,6 @@ lemma MulEquiv.strictMono_subsemigroupCongr {G : Type*} [OrderedCommMonoid G] {S
 
 @[to_additive]
 lemma MulEquiv.strictMono_symm {G G' : Type*} [LinearOrderedCommMonoid G]
-    [LinearOrderedCommMonoid G'] {e : G ≃* G'} (he : StrictMono e) : StrictMono e.symm := by
+    [OrderedCommMonoid G'] {e : G ≃* G'} (he : StrictMono e) : StrictMono e.symm := by
   intro
   simp [← he.lt_iff_lt]

Mathlib/Algebra/Group/Submonoid/Operations.lean

@@ -630,7 +630,7 @@ theorem mem_mrange {f : F} {y : N} : y ∈ mrange f ↔ ∃ x, f x = y :=
   Iff.rfl
 
 @[to_additive]
-lemma mrange_comp {O : Type*} [Monoid O] (f : N →* O) (g : M →* N) :
+lemma mrange_comp {O : Type*} [MulOneClass O] (f : N →* O) (g : M →* N) :
     mrange (f.comp g) = (mrange g).map f := SetLike.coe_injective <| Set.range_comp f _
 
 @[to_additive]

Mathlib/Algebra/GroupWithZero/Hom.lean

@@ -151,6 +151,18 @@ protected lemma map_zero (f : α →*₀ β) : f 0 = 0 := f.map_zero'
 
 protected lemma map_mul (f : α →*₀ β) (a b : α) : f (a * b) = f a * f b := f.map_mul' a b
 
+@[simp]
+theorem map_ite_zero_one {F : Type*} [FunLike F α β] [MonoidWithZeroHomClass F α β] (f : F)
+    (p : Prop) [Decidable p] :
+    f (ite p 0 1) = ite p 0 1 := by
+  split_ifs with h <;> simp [h]
+
+@[simp]
+theorem map_ite_one_zero {F : Type*} [FunLike F α β] [MonoidWithZeroHomClass F α β] (f : F)
+    (p : Prop) [Decidable p] :
+    f (ite p 1 0) = ite p 1 0 := by
+  split_ifs with h <;> simp [h]
+
 /-- The identity map from a `MonoidWithZero` to itself. -/
 @[simps]
 def id (α : Type*) [MulZeroOneClass α] : α →*₀ α where

Mathlib/Algebra/Ring/Basic.lean

@@ -124,12 +124,12 @@ section NoZeroDivisors
 
 variable (α)
 
-lemma IsLeftCancelMulZero.to_noZeroDivisors [NonUnitalNonAssocSemiring α]
+lemma IsLeftCancelMulZero.to_noZeroDivisors [MulZeroClass α]
     [IsLeftCancelMulZero α] : NoZeroDivisors α where
   eq_zero_or_eq_zero_of_mul_eq_zero {x _} h :=
     or_iff_not_imp_left.mpr fun ne ↦ mul_left_cancel₀ ne ((mul_zero x).symm ▸ h)
 
-lemma IsRightCancelMulZero.to_noZeroDivisors [NonUnitalNonAssocSemiring α]
+lemma IsRightCancelMulZero.to_noZeroDivisors [MulZeroClass α]
     [IsRightCancelMulZero α] : NoZeroDivisors α where
   eq_zero_or_eq_zero_of_mul_eq_zero {_ y} h :=
     or_iff_not_imp_right.mpr fun ne ↦ mul_right_cancel₀ ne ((zero_mul y).symm ▸ h)

Mathlib/Algebra/Ring/Commute.lean

@@ -163,13 +163,14 @@ lemma sq_ne_one_iff : a ^ 2 ≠ 1 ↔ a ≠ 1 ∧ a ≠ -1 := sq_eq_one_iff.not.
 end Ring
 
 /-- Representation of a difference of two squares in a commutative ring as a product. -/
-theorem mul_self_sub_mul_self [CommRing R] (a b : R) : a * a - b * b = (a + b) * (a - b) :=
+theorem mul_self_sub_mul_self [NonUnitalNonAssocCommRing R] (a b : R) :
+    a * a - b * b = (a + b) * (a - b) :=
   (Commute.all a b).mul_self_sub_mul_self_eq
 
 theorem mul_self_sub_one [NonAssocRing R] (a : R) : a * a - 1 = (a + 1) * (a - 1) := by
   rw [← (Commute.one_right a).mul_self_sub_mul_self_eq, mul_one]
 
-theorem mul_self_eq_mul_self_iff [CommRing R] [NoZeroDivisors R] {a b : R} :
+theorem mul_self_eq_mul_self_iff [NonUnitalNonAssocCommRing R] [NoZeroDivisors R] {a b : R} :
     a * a = b * b ↔ a = b ∨ a = -b :=
   (Commute.all a b).mul_self_eq_mul_self_iff
 

Mathlib/Algebra/Ring/Equiv.lean

@@ -590,7 +590,7 @@ theorem coe_monoidHom_trans [NonAssocSemiring S'] (e₁ : R ≃+* S) (e₂ : S 
   rfl
 
 @[simp]
-theorem coe_addMonoidHom_trans [NonAssocSemiring S'] (e₁ : R ≃+* S) (e₂ : S ≃+* S') :
+theorem coe_addMonoidHom_trans [NonUnitalNonAssocSemiring S'] (e₁ : R ≃+* S) (e₂ : S ≃+* S') :
     (e₁.trans e₂ : R →+ S') = (e₂ : S →+ S').comp ↑e₁ :=
   rfl
 

Mathlib/Algebra/Ring/Hom/Defs.lean

@@ -463,18 +463,6 @@ protected theorem map_add (f : α →+* β) : ∀ a b, f (a + b) = f a + f b :=
 protected theorem map_mul (f : α →+* β) : ∀ a b, f (a * b) = f a * f b :=
   map_mul f
 
-@[simp]
-theorem map_ite_zero_one {F : Type*} [FunLike F α β] [RingHomClass F α β] (f : F)
-    (p : Prop) [Decidable p] :
-    f (ite p 0 1) = ite p 0 1 := by
-  split_ifs with h <;> simp [h]
-
-@[simp]
-theorem map_ite_one_zero {F : Type*} [FunLike F α β] [RingHomClass F α β] (f : F)
-    (p : Prop) [Decidable p] :
-    f (ite p 1 0) = ite p 1 0 := by
-  split_ifs with h <;> simp [h]
-
 /-- `f : α →+* β` has a trivial codomain iff `f 1 = 0`. -/
 theorem codomain_trivial_iff_map_one_eq_zero : (0 : β) = 1 ↔ f 1 = 0 := by rw [map_one, eq_comm]
 

Mathlib/Algebra/Ring/Int/Defs.lean

@@ -57,7 +57,7 @@ lemma cast_mul {α : Type*} [NonAssocRing α] : ∀ m n, ((m * n : ℤ) : α) =
     | succ m ih => simp_all [add_mul]
 
 /-- Note this holds in marginally more generality than `Int.cast_mul` -/
-lemma cast_mul_eq_zsmul_cast {α : Type*} [AddCommGroupWithOne α] :
+lemma cast_mul_eq_zsmul_cast {α : Type*} [AddGroupWithOne α] :
     ∀ m n : ℤ, ↑(m * n) = m • (n : α) :=
   fun m ↦ Int.induction_on m (by simp) (fun _ ih ↦ by simp [add_mul, add_zsmul, ih]) fun _ ih ↦ by
     simp only [sub_mul, one_mul, cast_sub, ih, sub_zsmul, one_zsmul, ← sub_eq_add_neg, forall_const]

Mathlib/Algebra/Ring/Invertible.lean

@@ -32,7 +32,8 @@ theorem one_sub_invOf_two [Ring α] [Invertible (2 : α)] : 1 - (⅟ 2 : α) = 
 theorem invOf_two_add_invOf_two [NonAssocSemiring α] [Invertible (2 : α)] :
     (⅟ 2 : α) + (⅟ 2 : α) = 1 := by rw [← two_mul, mul_invOf_self]
 
-theorem pos_of_invertible_cast [Semiring α] [Nontrivial α] (n : ℕ) [Invertible (n : α)] : 0 < n :=
+theorem pos_of_invertible_cast [NonAssocSemiring α] [Nontrivial α] (n : ℕ) [Invertible (n : α)] :
+    0 < n :=
   Nat.zero_lt_of_ne_zero fun h => Invertible.ne_zero (n : α) (h ▸ Nat.cast_zero)
 
 theorem invOf_add_invOf [Semiring α] (a b : α) [Invertible a] [Invertible b] :

Mathlib/Algebra/Ring/Parity.lean

@@ -70,7 +70,8 @@ lemma Even.trans_dvd (ha : Even a) (hab : a ∣ b) : Even b :=
 
 lemma Dvd.dvd.even (hab : a ∣ b) (ha : Even a) : Even b := ha.trans_dvd hab
 
-@[simp] lemma range_two_mul (α) [Semiring α] : Set.range (fun x : α ↦ 2 * x) = {a | Even a} := by
+@[simp] lemma range_two_mul (α) [NonAssocSemiring α] :
+    Set.range (fun x : α ↦ 2 * x) = {a | Even a} := by
   ext x
   simp [eq_comm, two_mul, Even]
 

Mathlib/Algebra/Ring/Prod.lean

@@ -330,8 +330,8 @@ def zeroRingProd : R ≃+* S × R where
 end RingEquiv
 
 /-- The product of two nontrivial rings is not a domain -/
-theorem false_of_nontrivial_of_product_domain (R S : Type*) [Ring R] [Ring S] [IsDomain (R × S)]
-    [Nontrivial R] [Nontrivial S] : False := by
+theorem false_of_nontrivial_of_product_domain (R S : Type*) [Semiring R] [Semiring S]
+    [IsDomain (R × S)] [Nontrivial R] [Nontrivial S] : False := by
   have :=
     NoZeroDivisors.eq_zero_or_eq_zero_of_mul_eq_zero (show ((0 : R), (1 : S)) * (1, 0) = 0 by simp)
   rw [Prod.mk_eq_zero, Prod.mk_eq_zero] at this

Mathlib/Algebra/Ring/Subsemiring/Defs.lean

@@ -105,7 +105,7 @@ instance (priority := 75) toSemiring {R} [Semiring R] [SetLike S R] [Subsemiring
     (fun _ _ => rfl) (fun _ _ => rfl) fun _ => rfl
 
 @[simp, norm_cast]
-theorem coe_pow {R} [Semiring R] [SetLike S R] [SubsemiringClass S R] (x : s) (n : ℕ) :
+theorem coe_pow {R} [Monoid R] [SetLike S R] [SubmonoidClass S R] (x : s) (n : ℕ) :
     ((x ^ n : s) : R) = (x : R) ^ n := by
   induction n with
   | zero => simp

Mathlib/Algebra/Ring/Units.lean

@@ -106,7 +106,7 @@ theorem IsUnit.sub_iff [Ring α] {x y : α} : IsUnit (x - y) ↔ IsUnit (y - x)
 namespace Units
 
 @[field_simps]
-theorem divp_add_divp [CommRing α] (a b : α) (u₁ u₂ : αˣ) :
+theorem divp_add_divp [CommSemiring α] (a b : α) (u₁ u₂ : αˣ) :
     a /ₚ u₁ + b /ₚ u₂ = (a * u₂ + u₁ * b) /ₚ (u₁ * u₂) := by
   simp only [divp, add_mul, mul_inv_rev, val_mul]
   rw [mul_comm (↑u₁ * b), mul_comm b]

Mathlib/RingTheory/Kaehler/JacobiZariski.lean

@@ -138,7 +138,7 @@ lemma CotangentSpace.compEquiv_symm_inr :
       Basis.repr_self, Basis.prod_repr_inl, map_zero, Finsupp.coe_zero,
       Pi.zero_apply, ne_eq, not_false_eq_true, Pi.single_eq_of_ne, Pi.single_apply,
       Finsupp.single_apply, ite_smul, one_smul, zero_smul, Sum.inr.injEq,
-        RingHom.map_ite_one_zero, reduceCtorEq, ↓reduceIte]
+      MonoidWithZeroHom.map_ite_one_zero, reduceCtorEq, ↓reduceIte]
 
 lemma CotangentSpace.compEquiv_symm_zero (x) :
     (compEquiv Q P).symm (0, x) =
@@ -158,9 +158,9 @@ lemma CotangentSpace.fst_compEquiv :
   obtain (i | i) := i <;>
     simp only [comp_vars, Basis.repr_symm_apply, Finsupp.linearCombination_single, Basis.prod_apply,
       LinearMap.coe_inl, LinearMap.coe_inr, Sum.elim_inl, Function.comp_apply, one_smul,
-      Basis.repr_self, Finsupp.single_apply, pderiv_X, Pi.single_apply, RingHom.map_ite_one_zero,
+      Basis.repr_self, Finsupp.single_apply, pderiv_X, Pi.single_apply,
       Sum.elim_inr, Function.comp_apply, Basis.baseChange_apply, one_smul,
-      map_zero, Finsupp.coe_zero, Pi.zero_apply, derivation_C]
+      MonoidWithZeroHom.map_ite_one_zero, map_zero, Finsupp.coe_zero, Pi.zero_apply, derivation_C]
 
 lemma CotangentSpace.fst_compEquiv_apply (x) :
     (compEquiv Q P x).1 = Extension.CotangentSpace.map (Q.ofComp P).toExtensionHom x :=

Mathlib/RingTheory/MvPowerSeries/Basic.lean

@@ -501,8 +501,8 @@ def map : MvPowerSeries σ R →+* MvPowerSeries σ S where
         classical
         rw [coeff_one, coeff_one]
         split_ifs with h
-        · simp only [RingHom.map_ite_one_zero, ite_true, map_one, h]
-        · simp only [RingHom.map_ite_one_zero, ite_false, map_zero, h]
+        · simp only [ite_true, map_one, h]
+        · simp only [ite_false, map_zero, h]
   map_add' φ ψ :=
     ext fun n => show f ((coeff R n) (φ + ψ)) = f ((coeff R n) φ) + f ((coeff R n) ψ) by simp
   map_mul' φ ψ :=

Mathlib/RingTheory/Trace/Basic.lean

@@ -490,7 +490,7 @@ lemma traceForm_dualBasis_powerBasis_eq [FiniteDimensional K L] [Algebra.IsSepar
     map_pow, RingHom.coe_coe, AlgHom.coe_coe, finset_sum_coeff, coeff_smul, coeff_map, smul_eq_mul,
     coeff_X_pow, ← Fin.ext_iff, @eq_comm _ i] at this
   rw [PowerBasis.coe_basis]
-  simp only [RingHom.map_ite_one_zero, traceForm_apply]
+  simp only [MonoidWithZeroHom.map_ite_one_zero, traceForm_apply]
   rw [← this, trace_eq_sum_embeddings (E := AlgebraicClosure K)]
   apply Finset.sum_congr rfl
   intro σ _