feat: generalize Mathlib.Algebra.BigOperators + CharP + Star + misc others (#23195)

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/AddConstMap/Basic.lean

@@ -128,7 +128,7 @@ theorem map_ofNat [AddMonoidWithOne G] [AddMonoidWithOne H] [AddConstMapClass F
     f ofNat(n) = f 0 + ofNat(n) := map_nat f n
 
 @[scoped simp]
-theorem map_const_add [AddCommSemigroup G] [Add H] [AddConstMapClass F G H a b]
+theorem map_const_add [AddCommMagma G] [Add H] [AddConstMapClass F G H a b]
     (f : F) (x : G) : f (a + x) = f x + b := by
   rw [add_comm, map_add_const]
 

Mathlib/Algebra/AlgebraicCard.lean

@@ -25,11 +25,12 @@ open Cardinal Polynomial
 
 namespace Algebraic
 
-theorem infinite_of_charZero (R A : Type*) [CommRing R] [IsDomain R] [Ring A] [Algebra R A]
-    [CharZero A] : { x : A | IsAlgebraic R x }.Infinite :=
-  infinite_of_injective_forall_mem Nat.cast_injective isAlgebraic_nat
+theorem infinite_of_charZero (R A : Type*) [CommRing R] [Ring A] [Algebra R A]
+    [CharZero A] : { x : A | IsAlgebraic R x }.Infinite := by
+  letI := MulActionWithZero.nontrivial R A
+  exact infinite_of_injective_forall_mem Nat.cast_injective isAlgebraic_nat
 
-theorem aleph0_le_cardinalMk_of_charZero (R A : Type*) [CommRing R] [IsDomain R] [Ring A]
+theorem aleph0_le_cardinalMk_of_charZero (R A : Type*) [CommRing R] [Ring A]
     [Algebra R A] [CharZero A] : ℵ₀ ≤ #{ x : A // IsAlgebraic R x } :=
   infinite_iff.1 (Set.infinite_coe_iff.2 <| infinite_of_charZero R A)
 
@@ -80,7 +81,7 @@ protected theorem countable : Set.Countable { x : A | IsAlgebraic R x } := by
   simp
 
 @[simp]
-theorem cardinalMk_of_countable_of_charZero [CharZero A] [IsDomain R] :
+theorem cardinalMk_of_countable_of_charZero [CharZero A] :
     #{ x : A // IsAlgebraic R x } = ℵ₀ :=
   (Algebraic.countable R A).le_aleph0.antisymm (aleph0_le_cardinalMk_of_charZero R A)
 

Mathlib/Algebra/BigOperators/Fin.lean

@@ -454,7 +454,7 @@ theorem prod_ofFn {n : ℕ} {f : Fin n → α} : (ofFn f).prod = ∏ i, f i :=
 end CommMonoid
 
 @[to_additive]
-theorem alternatingProd_eq_finset_prod {G : Type*} [CommGroup G] :
+theorem alternatingProd_eq_finset_prod {G : Type*} [DivisionCommMonoid G] :
     ∀ (L : List G), alternatingProd L = ∏ i : Fin L.length, L[i] ^ (-1 : ℤ) ^ (i : ℕ)
   | [] => by
     rw [alternatingProd, Finset.prod_eq_one]

Mathlib/Algebra/BigOperators/Finprod.lean

@@ -304,8 +304,8 @@ theorem finsum_smul {R M : Type*} [Ring R] [AddCommGroup M] [Module R M] [NoZero
 
 /-- The `NoZeroSMulDivisors` makes sure that the result holds even when the support of `f` is
 infinite. For a more usual version assuming `(support f).Finite` instead, see `smul_finsum'`. -/
-theorem smul_finsum {R M : Type*} [Ring R] [AddCommGroup M] [Module R M] [NoZeroSMulDivisors R M]
-    (c : R) (f : ι → M) : (c • ∑ᶠ i, f i) = ∑ᶠ i, c • f i := by
+theorem smul_finsum {R M : Type*} [Semiring R] [AddCommGroup M] [Module R M]
+    [NoZeroSMulDivisors R M] (c : R) (f : ι → M) : (c • ∑ᶠ i, f i) = ∑ᶠ i, c • f i := by
   rcases eq_or_ne c 0 with (rfl | hc)
   · simp
   · exact (smulAddHom R M c).map_finsum_of_injective (smul_right_injective M hc) _
@@ -1030,12 +1030,12 @@ theorem prod_finprod_comm (s : Finset α) (f : α → β → M) (h : ∀ a ∈ s
     (∏ a ∈ s, ∏ᶠ b : β, f a b) = ∏ᶠ b : β, ∏ a ∈ s, f a b :=
   (finprod_prod_comm s (fun b a => f a b) h).symm
 
-theorem mul_finsum {R : Type*} [Semiring R] (f : α → R) (r : R) (h : (support f).Finite) :
-    (r * ∑ᶠ a : α, f a) = ∑ᶠ a : α, r * f a :=
+theorem mul_finsum {R : Type*} [NonUnitalNonAssocSemiring R] (f : α → R) (r : R)
+    (h : (support f).Finite) : (r * ∑ᶠ a : α, f a) = ∑ᶠ a : α, r * f a :=
   (AddMonoidHom.mulLeft r).map_finsum h
 
-theorem finsum_mul {R : Type*} [Semiring R] (f : α → R) (r : R) (h : (support f).Finite) :
-    (∑ᶠ a : α, f a) * r = ∑ᶠ a : α, f a * r :=
+theorem finsum_mul {R : Type*} [NonUnitalNonAssocSemiring R] (f : α → R) (r : R)
+    (h : (support f).Finite) : (∑ᶠ a : α, f a) * r = ∑ᶠ a : α, f a * r :=
   (AddMonoidHom.mulRight r).map_finsum h
 
 @[to_additive (attr := simp)]

Mathlib/Algebra/BigOperators/GroupWithZero/Action.lean

@@ -94,8 +94,8 @@ end
 namespace List
 
 @[to_additive]
-theorem smul_prod [Monoid α] [Monoid β] [MulAction α β] [IsScalarTower α β β] [SMulCommClass α β β]
-    (l : List β) (m : α) :
+theorem smul_prod [Monoid α] [MulOneClass β] [MulAction α β] [IsScalarTower α β β]
+    [SMulCommClass α β β] (l : List β) (m : α) :
     m ^ l.length • l.prod = (l.map (m • ·)).prod := by
   induction l with
   | nil => simp

Mathlib/Algebra/BigOperators/Pi.lean

@@ -60,7 +60,7 @@ theorem prod_mk_prod {α β γ : Type*} [CommMonoid α] [CommMonoid β] (s : Fin
   Finset.induction_on s rfl (by simp +contextual [Prod.ext_iff])
 
 /-- decomposing `x : ι → R` as a sum along the canonical basis -/
-theorem pi_eq_sum_univ {ι : Type*} [Fintype ι] [DecidableEq ι] {R : Type*} [Semiring R]
+theorem pi_eq_sum_univ {ι : Type*} [Fintype ι] [DecidableEq ι] {R : Type*} [NonAssocSemiring R]
     (x : ι → R) : x = ∑ i, (x i) • fun j => if i = j then (1 : R) else 0 := by
   ext
   simp

Mathlib/Algebra/BigOperators/Ring/List.lean

@@ -89,7 +89,7 @@ lemma dvd_sum [NonUnitalSemiring R] {a} {l : List R} (h : ∀ x ∈ l, a ∣ x)
     rw [List.sum_cons]
     exact dvd_add (h _ mem_cons_self) (ih fun x hx ↦ h x (mem_cons_of_mem _ hx))
 
-@[simp] lemma sum_zipWith_distrib_left [Semiring R] (f : ι → κ → R) (a : R) :
+@[simp] lemma sum_zipWith_distrib_left [NonUnitalNonAssocSemiring R] (f : ι → κ → R) (a : R) :
     ∀ (l₁ : List ι) (l₂ : List κ),
       (zipWith (fun i j ↦ a * f i j) l₁ l₂).sum = a * (zipWith f l₁ l₂).sum
   | [], _ => by simp

Mathlib/Algebra/BigOperators/RingEquiv.lean

@@ -19,8 +19,8 @@ variable {α R S : Type*}
 protected theorem map_list_prod [Semiring R] [Semiring S] (f : R ≃+* S) (l : List R) :
     f l.prod = (l.map f).prod := map_list_prod f l
 
-protected theorem map_list_sum [NonAssocSemiring R] [NonAssocSemiring S] (f : R ≃+* S)
-    (l : List R) : f l.sum = (l.map f).sum := map_list_sum f l
+protected theorem map_list_sum [NonUnitalNonAssocSemiring R] [NonUnitalNonAssocSemiring S]
+    (f : R ≃+* S) (l : List R) : f l.sum = (l.map f).sum := map_list_sum f l
 
 /-- An isomorphism into the opposite ring acts on the product by acting on the reversed elements -/
 protected theorem unop_map_list_prod [Semiring R] [Semiring S] (f : R ≃+* Sᵐᵒᵖ) (l : List R) :
@@ -31,16 +31,16 @@ protected theorem map_multiset_prod [CommSemiring R] [CommSemiring S] (f : R ≃
     (s : Multiset R) : f s.prod = (s.map f).prod :=
   map_multiset_prod f s
 
-protected theorem map_multiset_sum [NonAssocSemiring R] [NonAssocSemiring S] (f : R ≃+* S)
-    (s : Multiset R) : f s.sum = (s.map f).sum :=
+protected theorem map_multiset_sum [NonUnitalNonAssocSemiring R] [NonUnitalNonAssocSemiring S]
+    (f : R ≃+* S) (s : Multiset R) : f s.sum = (s.map f).sum :=
   map_multiset_sum f s
 
 protected theorem map_prod [CommSemiring R] [CommSemiring S] (g : R ≃+* S) (f : α → R)
     (s : Finset α) : g (∏ x ∈ s, f x) = ∏ x ∈ s, g (f x) :=
   map_prod g f s
 
-protected theorem map_sum [NonAssocSemiring R] [NonAssocSemiring S] (g : R ≃+* S) (f : α → R)
-    (s : Finset α) : g (∑ x ∈ s, f x) = ∑ x ∈ s, g (f x) :=
+protected theorem map_sum [NonUnitalNonAssocSemiring R] [NonUnitalNonAssocSemiring S] (g : R ≃+* S)
+    (f : α → R) (s : Finset α) : g (∑ x ∈ s, f x) = ∑ x ∈ s, g (f x) :=
   map_sum g f s
 
 end RingEquiv

Mathlib/Algebra/CharP/Algebra.lean

@@ -35,7 +35,7 @@ theorem CharP.dvd_of_ringHom {R A : Type*} [NonAssocSemiring R] [NonAssocSemirin
   rw [← map_natCast f p, CharP.cast_eq_zero, map_zero]
 
 /-- Given `R →+* A`, where `R` is a domain with `char R > 0`, then `char A = char R`. -/
-theorem CharP.of_ringHom_of_ne_zero {R A : Type*} [Ring R] [NoZeroDivisors R]
+theorem CharP.of_ringHom_of_ne_zero {R A : Type*} [NonAssocSemiring R] [NoZeroDivisors R]
     [NonAssocSemiring A] [Nontrivial A]
     (f : R →+* A) (p : ℕ) (hp : p ≠ 0) [CharP R p] : CharP A p := by
   have := f.domain_nontrivial
@@ -88,23 +88,23 @@ protected theorem RingHom.charP_iff {R A : Type*} [NonAssocSemiring R] [NonAssoc
 /-- If a ring homomorphism `R →+* A` is injective then `A` has the same exponential characteristic
 as `R`. -/
 lemma expChar_of_injective_ringHom {R A : Type*}
-    [Semiring R] [Semiring A] {f : R →+* A} (h : Function.Injective f)
+    [NonAssocSemiring R] [NonAssocSemiring A] {f : R →+* A} (h : Function.Injective f)
     (q : ℕ) [hR : ExpChar R q] : ExpChar A q := by
   rcases hR with _ | hprime
   · haveI := charZero_of_injective_ringHom h; exact .zero
   haveI := charP_of_injective_ringHom h q; exact .prime hprime
 
 /-- If `R →+* A` is injective, and `A` is of exponential characteristic `p`, then `R` is also of
 exponential characteristic `p`. Similar to `RingHom.charZero`. -/
-lemma RingHom.expChar {R A : Type*} [Semiring R] [Semiring A] (f : R →+* A)
+lemma RingHom.expChar {R A : Type*} [NonAssocSemiring R] [NonAssocSemiring A] (f : R →+* A)
     (H : Function.Injective f) (p : ℕ) [ExpChar A p] : ExpChar R p := by
   cases ‹ExpChar A p› with
   | zero => haveI := f.charZero; exact .zero
   | prime hp => haveI := f.charP H p; exact .prime hp
 
 /-- If `R →+* A` is injective, then `R` is of exponential characteristic `p` if and only if `A` is
 also of exponential characteristic `p`. Similar to `RingHom.charZero_iff`. -/
-lemma RingHom.expChar_iff {R A : Type*} [Semiring R] [Semiring A] (f : R →+* A)
+lemma RingHom.expChar_iff {R A : Type*} [NonAssocSemiring R] [NonAssocSemiring A] (f : R →+* A)
     (H : Function.Injective f) (p : ℕ) : ExpChar R p ↔ ExpChar A p :=
   ⟨fun _ ↦ expChar_of_injective_ringHom H p, fun _ ↦ f.expChar H p⟩
 
@@ -149,7 +149,7 @@ end QAlgebra
 An algebra over a field has the same characteristic as the field.
 -/
 
-lemma RingHom.charP_iff_charP {K L : Type*} [DivisionRing K] [Semiring L] [Nontrivial L]
+lemma RingHom.charP_iff_charP {K L : Type*} [DivisionRing K] [NonAssocSemiring L] [Nontrivial L]
     (f : K →+* L) (p : ℕ) : CharP K p ↔ CharP L p := by
   simp only [charP_iff, ← f.injective.eq_iff, map_natCast f, map_zero f]
 

Mathlib/Algebra/CharP/Defs.lean

@@ -166,7 +166,8 @@ lemma Nat.cast_ringChar : (ringChar R : R) = 0 := by rw [ringChar.spec]
 
 end ringChar
 
-lemma CharP.neg_one_ne_one [Ring R] (p : ℕ) [CharP R p] [Fact (2 < p)] : (-1 : R) ≠ (1 : R) := by
+lemma CharP.neg_one_ne_one [AddGroupWithOne R] (p : ℕ) [CharP R p] [Fact (2 < p)] :
+    (-1 : R) ≠ (1 : R) := by
   rw [ne_comm, ← sub_ne_zero, sub_neg_eq_add, one_add_one_eq_two, ← Nat.cast_two, Ne,
     CharP.cast_eq_zero_iff R p 2]
   exact fun h ↦ (Fact.out : 2 < p).not_le <| Nat.le_of_dvd Nat.zero_lt_two h