chore(algebra/group_hom): rename add_monoid.smul to nsmul (#2861)

Also drop `•` as a notation for two `smul`s  declared in this file,
use `•ℕ` and `•ℤ` instead.

This way one can immediately see that a lemma uses `nsmul`/`gsmul`, not `has_scalar.smul`.

Author: urkud

src/algebra/archimedean.lean

@@ -10,15 +10,13 @@ import data.rat
 
 variables {α : Type*}
 
-open_locale add_monoid
-
 class archimedean (α) [ordered_add_comm_monoid α] : Prop :=
-(arch : ∀ (x : α) {y}, 0 < y → ∃ n : ℕ, x ≤ n • y)
+(arch : ∀ (x : α) {y}, 0 < y → ∃ n : ℕ, x ≤ n •ℕ y)
 
 theorem exists_nat_gt [linear_ordered_semiring α] [archimedean α]
   (x : α) : ∃ n : ℕ, x < n :=
 let ⟨n, h⟩ := archimedean.arch x zero_lt_one in
-⟨n+1, lt_of_le_of_lt (by rwa ← add_monoid.smul_one)
+⟨n+1, lt_of_le_of_lt (by rwa ← nsmul_one)
   (nat.cast_lt.2 (nat.lt_succ_self _))⟩
 
 section linear_ordered_ring
@@ -30,8 +28,8 @@ have hy0 : 0 < y - 1 := sub_pos_of_lt hy1,
 -- TODO `by linarith` fails to prove hy1'
 have hy1' : (-1:α) ≤ y, from le_trans (neg_le_self zero_le_one) (le_of_lt hy1),
 let ⟨n, h⟩ := archimedean.arch x hy0 in
-⟨n, calc x ≤ n • (y - 1)     : h
-       ... < 1 + n • (y - 1) : lt_one_add _
+⟨n, calc x ≤ n •ℕ (y - 1)     : h
+       ... < 1 + n •ℕ (y - 1) : lt_one_add _
        ... ≤ y ^ n           : one_add_sub_mul_le_pow hy1' n⟩
 
 /-- Every x greater than 1 is between two successive natural-number
@@ -124,11 +122,11 @@ end
 end linear_ordered_field
 
 instance : archimedean ℕ :=
-⟨λ n m m0, ⟨n, by simpa only [mul_one, nat.smul_eq_mul] using nat.mul_le_mul_left n m0⟩⟩
+⟨λ n m m0, ⟨n, by simpa only [mul_one, nat.nsmul_eq_mul] using nat.mul_le_mul_left n m0⟩⟩
 
 instance : archimedean ℤ :=
 ⟨λ n m m0, ⟨n.to_nat, le_trans (int.le_to_nat _) $
-by simpa only [add_monoid.smul_eq_mul, int.nat_cast_eq_coe_nat, zero_add, mul_one] using mul_le_mul_of_nonneg_left
+by simpa only [nsmul_eq_mul, int.nat_cast_eq_coe_nat, zero_add, mul_one] using mul_le_mul_of_nonneg_left
     (int.add_one_le_iff.2 m0) (int.coe_zero_le n.to_nat)⟩⟩
 
 noncomputable def archimedean.floor_ring (α)
@@ -143,7 +141,7 @@ theorem archimedean_iff_nat_lt :
   archimedean α ↔ ∀ x : α, ∃ n : ℕ, x < n :=
 ⟨@exists_nat_gt α _, λ H, ⟨λ x y y0,
   (H (x / y)).imp $ λ n h, le_of_lt $
-  by rwa [div_lt_iff y0, ← add_monoid.smul_eq_mul] at h⟩⟩
+  by rwa [div_lt_iff y0, ← nsmul_eq_mul] at h⟩⟩
 
 theorem archimedean_iff_nat_le :
   archimedean α ↔ ∀ x : α, ∃ n : ℕ, x ≤ n :=

src/algebra/big_operators.lean

@@ -742,26 +742,26 @@ lemma sum_update_of_mem [add_comm_monoid β] [decidable_eq α] {s : finset α} {
 by { rw [update_eq_piecewise, sum_piecewise], simp [h] }
 attribute [to_additive] prod_update_of_mem
 
-lemma sum_smul' [add_comm_monoid β] (s : finset α) (n : ℕ) (f : α → β) :
-  (∑ x in s, add_monoid.smul n (f x)) = add_monoid.smul n ((∑ x in s, f x)) :=
+lemma sum_nsmul [add_comm_monoid β] (s : finset α) (n : ℕ) (f : α → β) :
+  (∑ x in s, n •ℕ (f x)) = n •ℕ ((∑ x in s, f x)) :=
 @prod_pow _ (multiplicative β) _ _ _ _
-attribute [to_additive sum_smul'] prod_pow
+attribute [to_additive sum_nsmul] prod_pow
 
 @[simp] lemma sum_const [add_comm_monoid β] (b : β) :
-  (∑ x in s, b) = add_monoid.smul s.card b :=
+  (∑ x in s, b) = s.card •ℕ b :=
 @prod_const _ (multiplicative β) _ _ _
 attribute [to_additive] prod_const
 
 lemma sum_comp [add_comm_monoid β] [decidable_eq γ] {s : finset α} (f : γ → β) (g : α → γ) :
-  ∑ a in s, f (g a) = ∑ b in s.image g, add_monoid.smul (s.filter (λ a, g a = b)).card (f b) :=
+  ∑ a in s, f (g a) = ∑ b in s.image g, (s.filter (λ a, g a = b)).card •ℕ (f b) :=
 @prod_comp _ (multiplicative β) _ _ _ _ _ _
 attribute [to_additive "The sum of the composition of functions `f` and `g`, is the sum
 over `b ∈ s.image g` of `f b` times of the cardinality of the fibre of `b`"] prod_comp
 
 lemma sum_const_nat {m : ℕ} {f : α → ℕ} (h₁ : ∀x ∈ s, f x = m) :
   (∑ x in s, f x) = card s * m :=
 begin
-  rw [← nat.smul_eq_mul, ← sum_const],
+  rw [← nat.nsmul_eq_mul, ← sum_const],
   apply sum_congr rfl h₁
 end
 
@@ -1238,7 +1238,7 @@ calc (∑ i in range n, i) * 2 = (∑ i in range n, i) + (∑ i in range n, (n -
 ... = ∑ i in range n, (i + (n - 1 - i)) : sum_add_distrib.symm
 ... = ∑ i in range n, (n - 1) : sum_congr rfl $ λ i hi, nat.add_sub_cancel' $
   nat.le_pred_of_lt $ mem_range.1 hi
-... = n * (n - 1) : by rw [sum_const, card_range, nat.smul_eq_mul]
+... = n * (n - 1) : by rw [sum_const, card_range, nat.nsmul_eq_mul]
 
 /-- Gauss' summation formula -/
 lemma sum_range_id (n : ℕ) : (∑ i in range n, i) = (n * (n - 1)) / 2 :=

src/algebra/commute.lean

@@ -34,8 +34,6 @@ Most of the proofs come from the properties of `semiconj_by`.
 /-- Two elements commute iff `a * b = b * a`. -/
 def commute {S : Type*} [has_mul S] (a b : S) : Prop := semiconj_by a b b
 
-open_locale smul
-
 namespace commute
 
 section has_mul
@@ -167,15 +165,15 @@ semiconj_by.add_left
 
 variables [semiring A] {a b : A} (hab : commute a b) (m n : ℕ)
 
-@[simp] theorem smul_right : commute a (n •ℕ b) := hab.smul_right n
-@[simp] theorem smul_left : commute (n •ℕ a) b := hab.smul_left n
-@[simp] theorem smul_smul : commute (m •ℕ a) (n •ℕ b) := hab.smul_smul m n
+@[simp] theorem nsmul_right : commute a (n •ℕ b) := hab.nsmul_right n
+@[simp] theorem nsmul_left : commute (n •ℕ a) b := hab.nsmul_left n
+@[simp] theorem nsmul_nsmul : commute (m •ℕ a) (n •ℕ b) := hab.nsmul_nsmul m n
 
 variable (a)
 
-@[simp] theorem self_smul : commute a (n •ℕ a) := (commute.refl a).smul_right n
-@[simp] theorem smul_self : commute (n •ℕ a) a := (commute.refl a).smul_left n
-@[simp] theorem self_smul_smul : commute (m •ℕ a) (n •ℕ a) := (commute.refl a).smul_smul m n
+@[simp] theorem self_nsmul : commute a (n •ℕ a) := (commute.refl a).nsmul_right n
+@[simp] theorem nsmul_self : commute (n •ℕ a) a := (commute.refl a).nsmul_left n
+@[simp] theorem self_nsmul_nsmul : commute (m •ℕ a) (n •ℕ a) := (commute.refl a).nsmul_nsmul m n
 
 @[simp] theorem cast_nat_right : commute a (n : A) := semiconj_by.cast_nat_right a n
 @[simp] theorem cast_nat_left : commute (n : A) a := semiconj_by.cast_nat_left n a

src/algebra/geom_sum.lean

@@ -84,8 +84,8 @@ calc  (finset.range n).sum (λ i, x ^ i * x ^ (n - 1 - i))
     = (finset.range n).sum (λ i, x ^ (i + (n - 1 - i))) : by simp_rw [← pow_add]
 ... = (finset.range n).sum (λ i, x ^ (n - 1)) : finset.sum_congr rfl
   (λ i hi, congr_arg _ $ nat.add_sub_cancel' $ nat.le_pred_of_lt $ finset.mem_range.1 hi)
-... = add_monoid.smul (finset.range n).card (x ^ (n - 1)) : finset.sum_const _
-... = n * x ^ (n - 1) : by rw [finset.card_range, add_monoid.smul_eq_mul]
+... = (finset.range n).card •ℕ (x ^ (n - 1)) : finset.sum_const _
+... = n * x ^ (n - 1) : by rw [finset.card_range, nsmul_eq_mul]
 
 /-- $x^n-y^n = (x-y) \sum x^ky^{n-1-k}$ reformulated without `-` signs. -/
 theorem geom_sum₂_mul_add [comm_semiring α] (x y : α) (n : ℕ) :