chore(algebra/*): generalisation linter (replacing ring with non_asso…

…c_ring) (#13106)




Co-authored-by: Scott Morrison <scott.morrison@gmail.com>

src/algebra/big_operators/multiset.lean

@@ -233,7 +233,7 @@ by { convert (m.map f).prod_hom (zpow_group_hom₀ _ : α →* α), rw map_map,
 
 end comm_group_with_zero
 
-section semiring
+section non_unital_non_assoc_semiring
 variables [non_unital_non_assoc_semiring α] {a : α} {s : multiset ι} {f : ι → α}
 
 lemma _root_.commute.multiset_sum_right (s : multiset α) (a : α) (h : ∀ b ∈ s, commute a b) :
@@ -254,17 +254,17 @@ multiset.induction_on s (by simp) (λ i s ih, by simp [ih, mul_add])
 lemma sum_map_mul_right : sum (s.map (λ i, f i * a)) = sum (s.map f) * a :=
 multiset.induction_on s (by simp) (λ a s ih, by simp [ih, add_mul])
 
-end semiring
+end non_unital_non_assoc_semiring
 
-section comm_semiring
-variables [comm_semiring α]
+section semiring
+variables [semiring α]
 
 lemma dvd_sum {a : α} {s : multiset α} : (∀ x ∈ s, a ∣ x) → a ∣ s.sum :=
 multiset.induction_on s (λ _, dvd_zero _)
   (λ x s ih h, by { rw sum_cons, exact dvd_add
     (h _ (mem_cons_self _ _)) (ih $ λ y hy, h _ $ mem_cons.2 $ or.inr hy) })
 
-end comm_semiring
+end semiring
 
 /-! ### Order -/
 

src/algebra/big_operators/pi.lean

@@ -84,10 +84,10 @@ end single
 section ring_hom
 open pi
 variables {I : Type*} [decidable_eq I] {f : I → Type*}
-variables [Π i, semiring (f i)]
+variables [Π i, non_assoc_semiring (f i)]
 
-@[ext] lemma ring_hom.functions_ext [fintype I] (G : Type*) [semiring G] (g h : (Π i, f i) →+* G)
-  (w : ∀ (i : I) (x : f i), g (single i x) = h (single i x)) : g = h :=
+@[ext] lemma ring_hom.functions_ext [fintype I] (G : Type*) [non_assoc_semiring G]
+  (g h : (Π i, f i) →+* G) (w : ∀ (i : I) (x : f i), g (single i x) = h (single i x)) : g = h :=
 ring_hom.coe_add_monoid_hom_injective $
  add_monoid_hom.functions_ext G (g : (Π i, f i) →+ G) h w
 

src/algebra/big_operators/ring.lean

@@ -24,6 +24,21 @@ variables {α : Type u} {β : Type v} {γ : Type w}
 namespace finset
 variables {s s₁ s₂ : finset α} {a : α} {b : β}  {f g : α → β}
 
+section comm_monoid
+variables [comm_monoid β]
+
+open_locale classical
+
+lemma prod_pow_eq_pow_sum {x : β} {f : α → ℕ} :
+  ∀ {s : finset α}, (∏ i in s, x ^ (f i)) = x ^ (∑ x in s, f x) :=
+begin
+  apply finset.induction,
+  { simp },
+  { assume a s has H,
+    rw [finset.prod_insert has, finset.sum_insert has, pow_add, H] }
+end
+
+end comm_monoid
 
 section semiring
 variables [non_unital_non_assoc_semiring β]
@@ -180,15 +195,6 @@ begin
   rw [prod_const, prod_const, ← card_sdiff (mem_powerset.1 ht)]
 end
 
-lemma prod_pow_eq_pow_sum {x : β} {f : α → ℕ} :
-  ∀ {s : finset α}, (∏ i in s, x ^ (f i)) = x ^ (∑ x in s, f x) :=
-begin
-  apply finset.induction,
-  { simp },
-  { assume a s has H,
-    rw [finset.prod_insert has, finset.sum_insert has, pow_add, H] }
-end
-
 theorem dvd_sum {b : β} {s : finset α} {f : α → β}
   (h : ∀ x ∈ s, b ∣ f x) : b ∣ ∑ x in s, f x :=
 multiset.dvd_sum (λ y hy, by rcases multiset.mem_map.1 hy with ⟨x, hx, rfl⟩; exact h x hx)

src/algebra/char_zero.lean

@@ -128,7 +128,7 @@ by rwa [nat.cast_two] at this
 end
 
 section
-variables {R : Type*} [semiring R] [no_zero_divisors R] [char_zero R]
+variables {R : Type*} [non_assoc_semiring R] [no_zero_divisors R] [char_zero R]
 
 @[simp]
 lemma add_self_eq_zero {a : R} : a + a = 0 ↔ a = 0 :=
@@ -142,7 +142,7 @@ by { rw [eq_comm], exact bit0_eq_zero }
 end
 
 section
-variables {R : Type*} [ring R] [no_zero_divisors R] [char_zero R]
+variables {R : Type*} [non_assoc_ring R] [no_zero_divisors R] [char_zero R]
 
 lemma neg_eq_self_iff {a : R} : -a = a ↔ a = 0 :=
 neg_eq_iff_add_eq_zero.trans add_self_eq_zero
@@ -215,7 +215,7 @@ end with_top
 
 section ring_hom
 
-variables {R S : Type*} [semiring R] [semiring S]
+variables {R S : Type*} [non_assoc_semiring R] [non_assoc_semiring S]
 
 lemma ring_hom.char_zero (ϕ : R →+* S) [hS : char_zero S] : char_zero R :=
 ⟨λ a b h, char_zero.cast_injective (by rw [←map_nat_cast ϕ, ←map_nat_cast ϕ, h])⟩

src/algebra/group_power/lemmas.lean

@@ -335,11 +335,11 @@ end linear_ordered_add_comm_group
   ((n • a : A) : with_bot A) = n • a :=
 add_monoid_hom.map_nsmul ⟨(coe : A → with_bot A), with_bot.coe_zero, with_bot.coe_add⟩ a n
 
-theorem nsmul_eq_mul' [semiring R] (a : R) (n : ℕ) : n • a = a * n :=
+theorem nsmul_eq_mul' [non_assoc_semiring R] (a : R) (n : ℕ) : n • a = a * n :=
 by induction n with n ih; [rw [zero_nsmul, nat.cast_zero, mul_zero],
   rw [succ_nsmul', ih, nat.cast_succ, mul_add, mul_one]]
 
-@[simp] theorem nsmul_eq_mul [semiring R] (n : ℕ) (a : R) : n • a = n * a :=
+@[simp] theorem nsmul_eq_mul [non_assoc_semiring R] (n : ℕ) (a : R) : n • a = n * a :=
 by rw [nsmul_eq_mul', (n.cast_commute a).eq]
 
 /-- Note that `add_comm_monoid.nat_smul_comm_class` requires stronger assumptions on `R`. -/
@@ -374,19 +374,19 @@ by induction k with k ih; [refl, rw [pow_succ', int.nat_abs_mul, pow_succ', ih]]
 -- The next four lemmas allow us to replace multiplication by a numeral with a `zsmul` expression.
 -- They are used by the `noncomm_ring` tactic, to normalise expressions before passing to `abel`.
 
-lemma bit0_mul [ring R] {n r : R} : bit0 n * r = (2 : ℤ) • (n * r) :=
+lemma bit0_mul [non_unital_non_assoc_ring R] {n r : R} : bit0 n * r = (2 : ℤ) • (n * r) :=
 by { dsimp [bit0], rw [add_mul, add_zsmul, one_zsmul], }
 
-lemma mul_bit0 [ring R] {n r : R} : r * bit0 n = (2 : ℤ) • (r * n) :=
+lemma mul_bit0 [non_unital_non_assoc_ring R] {n r : R} : r * bit0 n = (2 : ℤ) • (r * n) :=
 by { dsimp [bit0], rw [mul_add, add_zsmul, one_zsmul], }
 
-lemma bit1_mul [ring R] {n r : R} : bit1 n * r = (2 : ℤ) • (n * r) + r :=
+lemma bit1_mul [non_assoc_ring R] {n r : R} : bit1 n * r = (2 : ℤ) • (n * r) + r :=
 by { dsimp [bit1], rw [add_mul, bit0_mul, one_mul], }
 
-lemma mul_bit1 [ring R] {n r : R} : r * bit1 n = (2 : ℤ) • (r * n) + r :=
+lemma mul_bit1 [non_assoc_ring R] {n r : R} : r * bit1 n = (2 : ℤ) • (r * n) + r :=
 by { dsimp [bit1], rw [mul_add, mul_bit0, mul_one], }
 
-@[simp] theorem zsmul_eq_mul [ring R] (a : R) : ∀ (n : ℤ), n • a = n * a
+@[simp] theorem zsmul_eq_mul [non_assoc_ring R] (a : R) : ∀ (n : ℤ), n • a = n * a
 | (n : ℕ) := by { rw [coe_nat_zsmul, nsmul_eq_mul], refl }
 | -[1+ n] := by simp [nat.cast_succ, neg_add_rev, int.cast_neg_succ_of_nat, add_mul]
 

src/algebra/ring/equiv.lean

@@ -321,7 +321,7 @@ end semiring
 
 section
 
-variables [ring R] [ring S] (f : R ≃+* S) (x y : R)
+variables [non_assoc_ring R] [non_assoc_ring S] (f : R ≃+* S) (x y : R)
 
 protected lemma map_neg : f (-x) = -f x := map_neg f x
 

src/ring_theory/subring/basic.lean

@@ -911,7 +911,7 @@ end subring
 
 namespace ring_hom
 
-variables [ring T] {s : subring R}
+variables {s : subring R}
 
 open subring