feat(algebra/group/to_additive): let to_additive turn pow into `nsm…

…ul` (#12477)

The naming convention for `npow` in lemma names is `pow`, so let’s teach
`to_additive` about it.

A fair number of lemmas now no longer need an explicit additive name.

src/algebra/big_operators/basic.lean

@@ -1035,7 +1035,7 @@ by rw [prod_insert has, card_insert_of_not_mem has, pow_succ, ih])
 @[to_additive]
 lemma pow_eq_prod_const (b : β) : ∀ n, b ^ n = ∏ k in range n, b := by simp
 
-@[to_additive sum_nsmul]
+@[to_additive]
 lemma prod_pow (s : finset α) (n : ℕ) (f : α → β) :
   ∏ x in s, f x ^ n = (∏ x in s, f x) ^ n :=
 by haveI := classical.dec_eq α; exact

src/algebra/big_operators/multiset.lean

@@ -70,7 +70,7 @@ lemma prod_nsmul (m : multiset α) : ∀ (n : ℕ), (n • m).prod = m.prod ^ n
 @[simp, to_additive] lemma prod_repeat (a : α) (n : ℕ) : (repeat a n).prod = a ^ n :=
 by simp [repeat, list.prod_repeat]
 
-@[to_additive nsmul_count]
+@[to_additive]
 lemma pow_count [decidable_eq α] (a : α) : a ^ s.count a = (s.filter (eq a)).prod :=
 by rw [filter_eq, prod_repeat]
 
@@ -105,7 +105,7 @@ lemma prod_map_one : prod (m.map (λ i, (1 : α))) = 1 := by rw [map_const, prod
 lemma prod_map_mul : (m.map $ λ i, f i * g i).prod = (m.map f).prod * (m.map g).prod :=
 m.prod_hom₂ (*) mul_mul_mul_comm (mul_one _) _ _
 
-@[to_additive sum_map_nsmul]
+@[to_additive]
 lemma prod_map_pow {n : ℕ} : (m.map $ λ i, f i ^ n).prod = (m.map f).prod ^ n :=
 m.prod_hom' (pow_monoid_hom n : α →* α) f
 

src/algebra/group/hom.lean

@@ -305,7 +305,7 @@ by rw [map_mul, map_inv]
   (f : F) (x y : G) : f (x / y) = f x / f y :=
 by rw [div_eq_mul_inv, div_eq_mul_inv, map_mul_inv]
 
-@[simp, to_additive map_nsmul] theorem map_pow [monoid G] [monoid H] [monoid_hom_class F G H]
+@[simp, to_additive] theorem map_pow [monoid G] [monoid H] [monoid_hom_class F G H]
   (f : F) (a : G) :
   ∀ (n : ℕ), f (a ^ n) = (f a) ^ n
 | 0     := by rw [pow_zero, pow_zero, map_one]

src/algebra/group/pi.lean

@@ -43,7 +43,7 @@ by refine_struct { one := (1 : Π i, f i), mul := (*), npow := λ n x i, (x i) ^
 tactic.pi_instance_derive_field
 
 -- the attributes are intentionally out of order. `smul_apply` proves `nsmul_apply`.
-@[to_additive nsmul_apply, simp]
+@[to_additive, simp]
 lemma pow_apply [∀ i, monoid $ f i] (n : ℕ) : (x^n) i = (x i)^n := rfl
 
 @[to_additive]

src/algebra/group/to_additive.lean

@@ -213,6 +213,7 @@ meta def tr : bool → list string → list string
 | is_comm ("one" :: s)                := add_comm_prefix is_comm "zero"      :: tr ff s
 | is_comm ("prod" :: s)               := add_comm_prefix is_comm "sum"       :: tr ff s
 | is_comm ("finprod" :: s)            := add_comm_prefix is_comm "finsum"    :: tr ff s
+| is_comm ("pow" :: s)                := add_comm_prefix is_comm "nsmul"     :: tr ff s
 | is_comm ("npow" :: s)               := add_comm_prefix is_comm "nsmul"     :: tr ff s
 | is_comm ("zpow" :: s)               := add_comm_prefix is_comm "zsmul"     :: tr ff s
 | is_comm ("monoid" :: s)      := ("add_" ++ add_comm_prefix is_comm "monoid")    :: tr ff s

src/algebra/group_power/basic.lean

@@ -55,7 +55,7 @@ by rw [pow_succ, pow_one]
 
 alias pow_two ← sq
 
-@[to_additive nsmul_add_comm']
+@[to_additive]
 theorem pow_mul_comm' (a : M) (n : ℕ) : a^n * a = a * a^n := commute.pow_self a n
 
 @[to_additive add_nsmul]
@@ -110,7 +110,7 @@ theorem pow_bit0 (a : M) (n : ℕ) : a ^ bit0 n = a^n * a^n := pow_add _ _ _
 theorem pow_bit1 (a : M) (n : ℕ) : a ^ bit1 n = a^n * a^n * a :=
 by rw [bit1, pow_succ', pow_bit0]
 
-@[to_additive nsmul_add_comm]
+@[to_additive]
 theorem pow_mul_comm (a : M) (m n : ℕ) : a^m * a^n = a^n * a^m :=
 commute.pow_pow_self a m n
 
@@ -143,7 +143,7 @@ theorem mul_pow (a b : M) (n : ℕ) : (a * b)^n = a^n * b^n :=
 
 /-- The `n`th power map on a commutative monoid for a natural `n`, considered as a morphism of
 monoids. -/
-@[to_additive nsmul_add_monoid_hom "Multiplication by a natural `n` on a commutative additive
+@[to_additive "Multiplication by a natural `n` on a commutative additive
 monoid, considered as a morphism of additive monoids.", simps]
 def pow_monoid_hom (n : ℕ) : M →* M :=
 { to_fun := (^ n),
@@ -195,20 +195,20 @@ open int
 
 section nat
 
-@[simp, to_additive neg_nsmul] theorem inv_pow (a : G) (n : ℕ) : (a⁻¹)^n = (a^n)⁻¹ :=
+@[simp, to_additive] theorem inv_pow (a : G) (n : ℕ) : (a⁻¹)^n = (a^n)⁻¹ :=
 begin
   induction n with n ih,
   { rw [pow_zero, pow_zero, one_inv] },
   { rw [pow_succ', pow_succ, ih, mul_inv_rev] }
 end
 
-@[to_additive nsmul_sub] -- rename to sub_nsmul?
+@[to_additive] -- rename to sub_nsmul?
 theorem pow_sub (a : G) {m n : ℕ} (h : n ≤ m) : a^(m - n) = a^m * (a^n)⁻¹ :=
 have h1 : m - n + n = m, from tsub_add_cancel_of_le h,
 have h2 : a^(m - n) * a^n = a^m, by rw [←pow_add, h1],
 eq_mul_inv_of_mul_eq h2
 
-@[to_additive nsmul_neg_comm]
+@[to_additive]
 theorem pow_inv_comm (a : G) (m n : ℕ) : (a⁻¹)^m * a^n = a^n * (a⁻¹)^m :=
 (commute.refl a).inv_left.pow_pow m n
 

src/algebra/group_power/order.lean

@@ -81,19 +81,19 @@ variables [monoid M] [linear_order M] [covariant_class M M (*) (≤)]
 lemma one_le_pow_iff {x : M} {n : ℕ} (hn : n ≠ 0) : 1 ≤ x ^ n ↔ 1 ≤ x :=
 ⟨le_imp_le_of_lt_imp_lt $ λ h, pow_lt_one' h hn, λ h, one_le_pow_of_one_le' h n⟩
 
-@[to_additive nsmul_nonpos_iff]
+@[to_additive]
 lemma pow_le_one_iff {x : M} {n : ℕ} (hn : n ≠ 0) : x ^ n ≤ 1 ↔ x ≤ 1 :=
 @one_le_pow_iff (order_dual M) _ _ _ _ _ hn
 
 @[to_additive nsmul_pos_iff]
 lemma one_lt_pow_iff {x : M} {n : ℕ} (hn : n ≠ 0) : 1 < x ^ n ↔ 1 < x :=
 lt_iff_lt_of_le_iff_le (pow_le_one_iff hn)
 
-@[to_additive nsmul_neg_iff]
+@[to_additive]
 lemma pow_lt_one_iff {x : M} {n : ℕ} (hn : n ≠ 0) : x ^ n < 1 ↔ x < 1 :=
 lt_iff_lt_of_le_iff_le (one_le_pow_iff hn)
 
-@[to_additive nsmul_eq_zero_iff]
+@[to_additive]
 lemma pow_eq_one_iff {x : M} {n : ℕ} (hn : n ≠ 0) : x ^ n = 1 ↔ x = 1 :=
 by simp only [le_antisymm_iff, pow_le_one_iff hn, one_le_pow_iff hn]
 

src/algebra/iterate_hom.lean

@@ -86,7 +86,7 @@ theorem iterate_map_smul (f : M →+ M) (n m : ℕ) (x : M) :
   f^[n] (m • x) = m • (f^[n] x) :=
 f.to_multiplicative.iterate_map_pow n x m
 
-attribute [to_additive iterate_map_smul, to_additive_reorder 5] monoid_hom.iterate_map_pow
+attribute [to_additive, to_additive_reorder 5] monoid_hom.iterate_map_pow
 
 theorem iterate_map_zsmul (f : G →+ G) (n : ℕ) (m : ℤ) (x : G) :
   f^[n] (m • x) = m • (f^[n] x) :=

src/algebra/pointwise.lean

@@ -250,7 +250,7 @@ protected def comm_monoid [comm_monoid α] : comm_monoid (set α) :=
 localized "attribute [instance] set.mul_one_class set.add_zero_class set.semigroup set.add_semigroup
   set.monoid set.add_monoid set.comm_monoid set.add_comm_monoid" in pointwise
 
-@[to_additive nsmul_mem_nsmul]
+@[to_additive]
 lemma pow_mem_pow [monoid α] (ha : a ∈ s) (n : ℕ) :
   a ^ n ∈ s ^ n :=
 begin
@@ -261,7 +261,7 @@ begin
     exact set.mul_mem_mul ha ih },
 end
 
-@[to_additive empty_nsmul]
+@[to_additive]
 lemma empty_pow [monoid α] (n : ℕ) (hn : n ≠ 0) : (∅ : set α) ^ n = ∅ :=
 by rw [← tsub_add_cancel_of_le (nat.succ_le_of_lt $ nat.pos_of_ne_zero hn), pow_succ, empty_mul]
 

src/group_theory/exponent.lean

@@ -89,7 +89,7 @@ begin
   { simp_rw [exponent, dif_neg h, pow_zero] }
 end
 
-@[to_additive nsmul_eq_mod_exponent]
+@[to_additive]
 lemma pow_eq_mod_exponent {n : ℕ} (g : G): g ^ n = g ^ (n % exponent G) :=
 calc g ^ n = g ^ (n % exponent G + exponent G * (n / exponent G)) : by rw [nat.mod_add_div]
   ... = g ^ (n % exponent G) : by simp [pow_add, pow_mul, pow_exponent_eq_one]
@@ -138,7 +138,7 @@ order_of_dvd_of_pow_eq_one $ pow_exponent_eq_one g
 
 variable (G)
 
-@[to_additive exponent_dvd_of_forall_nsmul_eq_zero]
+@[to_additive]
 lemma exponent_dvd_of_forall_pow_eq_one (G) [monoid G] (n : ℕ) (hG : ∀ g : G, g ^ n = 1) :
   exponent G ∣ n :=
 begin

src/group_theory/order_of_element.lean

@@ -43,7 +43,7 @@ variables [monoid G] [add_monoid A]
 
 section is_of_fin_order
 
-@[to_additive is_periodic_pt_add_iff_nsmul_eq_zero]
+@[to_additive]
 lemma is_periodic_pt_mul_iff_pow_eq_one (x : G) : is_periodic_pt ((*) x) n 1 ↔ x ^ n = 1 :=
 by rw [is_periodic_pt, is_fixed_pt, mul_left_iterate, mul_one]
 
@@ -154,7 +154,7 @@ is_periodic_pt.minimal_period_dvd ((is_periodic_pt_mul_iff_pow_eq_one _).mpr h)
 lemma order_of_dvd_iff_pow_eq_one {n : ℕ} : order_of x ∣ n ↔ x ^ n = 1 :=
 ⟨λ h, by rw [pow_eq_mod_order_of, nat.mod_eq_zero_of_dvd h, pow_zero], order_of_dvd_of_pow_eq_one⟩
 
-@[to_additive exists_nsmul_eq_self_of_coprime]
+@[to_additive]
 lemma exists_pow_eq_self_of_coprime (h : n.coprime (order_of x)) :
   ∃ m : ℕ, (x ^ n) ^ m = x :=
 begin
@@ -285,7 +285,7 @@ end monoid_add_monoid
 section cancel_monoid
 variables [left_cancel_monoid G] (x y)
 
-@[to_additive nsmul_injective_aux]
+@[to_additive]
 lemma pow_injective_aux (h : n ≤ m)
   (hm : m < order_of x) (eq : x ^ n = x ^ m) : n = m :=
 by_contradiction $ assume ne : n ≠ m,
@@ -362,7 +362,7 @@ begin
     { simp [pow_succ, IH] } }
 end
 
-@[to_additive nsmul_inj_mod]
+@[to_additive]
 lemma pow_inj_mod {n m : ℕ} :
   x ^ n = x ^ m ↔ n % order_of x = m % order_of x :=
 begin
@@ -403,7 +403,7 @@ section finite_cancel_monoid
 variables [left_cancel_monoid G] [add_left_cancel_monoid A]
 
 -- TODO: Use this to show that a finite left cancellative monoid is a group.
-@[to_additive exists_nsmul_eq_zero]
+@[to_additive]
 lemma exists_pow_eq_one (x : G) : is_of_fin_order x :=
 begin
   refine (is_of_fin_order_iff_pow_eq_one _).mpr _,
@@ -612,7 +612,7 @@ end
 let ⟨m, hm⟩ := @order_of_dvd_card_univ _ x _ _ in
 by simp [hm, pow_mul, pow_order_of_eq_one]
 
-@[to_additive nsmul_eq_mod_card] lemma pow_eq_mod_card (n : ℕ) :
+@[to_additive] lemma pow_eq_mod_card (n : ℕ) :
   x ^ n = x ^ (n % fintype.card G) :=
 by rw [pow_eq_mod_order_of, ←nat.mod_mod_of_dvd n order_of_dvd_card_univ,
   ← pow_eq_mod_order_of]
@@ -623,7 +623,7 @@ by rw [zpow_eq_mod_order_of, ← int.mod_mod_of_dvd n (int.coe_nat_dvd.2 order_o
   ← zpow_eq_mod_order_of]
 
 /-- If `gcd(|G|,n)=1` then the `n`th power map is a bijection -/
-@[to_additive nsmul_coprime "If `gcd(|G|,n)=1` then the smul by `n` is a bijection", simps]
+@[to_additive "If `gcd(|G|,n)=1` then the smul by `n` is a bijection", simps]
   def pow_coprime (h : nat.coprime (fintype.card G) n) : G ≃ G :=
 { to_fun := λ g, g ^ n,
   inv_fun := λ g, g ^ (nat.gcd_b (fintype.card G) n),

src/group_theory/submonoid/membership.lean

@@ -40,7 +40,7 @@ namespace submonoid
 section assoc
 variables [monoid M] (S : submonoid M)
 
-@[simp, norm_cast, to_additive coe_nsmul] theorem coe_pow (x : S) (n : ℕ) :
+@[simp, norm_cast, to_additive] theorem coe_pow (x : S) (n : ℕ) :
   ↑(x ^ n) = (x ^ n : M) :=
 S.subtype.map_pow x n
 
@@ -78,7 +78,7 @@ lemma prod_mem {M : Type*} [comm_monoid M] (S : submonoid M)
   ∏ c in t, f c ∈ S :=
 S.multiset_prod_mem (t.1.map f) $ λ x hx, let ⟨i, hi, hix⟩ := multiset.mem_map.1 hx in hix ▸ h i hi
 
-@[to_additive nsmul_mem] lemma pow_mem {x : M} (hx : x ∈ S) (n : ℕ) : x ^ n ∈ S :=
+@[to_additive] lemma pow_mem {x : M} (hx : x ∈ S) (n : ℕ) : x ^ n ∈ S :=
 by simpa only [coe_pow] using ((⟨x, hx⟩ : S) ^ n).coe_prop
 
 end assoc

src/number_theory/divisors.lean

@@ -376,7 +376,7 @@ lemma prod_proper_divisors_prime_pow {α : Type*} [comm_monoid α] {k p : ℕ} {
   (h : p.prime) : ∏ x in (p ^ k).proper_divisors, f x = ∏ x in range k, f (p ^ x) :=
 by simp [h, proper_divisors_prime_pow]
 
-@[simp, to_additive]
+@[simp, to_additive sum_divisors_prime_pow]
 lemma prod_divisors_prime_pow {α : Type*} [comm_monoid α] {k p : ℕ} {f : ℕ → α} (h : p.prime) :
   ∏ x in (p ^ k).divisors, f x = ∏ x in range (k + 1), f (p ^ x) :=
 by simp [h, divisors_prime_pow]

src/topology/algebra/monoid.lean

@@ -372,7 +372,7 @@ lemma continuous_list_prod {f : ι → X → M} (l : list ι)
 continuous_iff_continuous_at.2 $ assume x, tendsto_list_prod l $ assume c hc,
   continuous_iff_continuous_at.1 (h c hc) x
 
-@[continuity, to_additive continuous_nsmul]
+@[continuity, to_additive]
 lemma continuous_pow : ∀ n : ℕ, continuous (λ a : M, a ^ n)
 | 0 := by simpa using continuous_const
 | (k+1) := by { simp only [pow_succ], exact continuous_id.mul (continuous_pow _) }
@@ -385,11 +385,11 @@ lemma continuous.pow {f : X → M} (h : continuous f) (n : ℕ) :
   continuous (λ b, (f b) ^ n) :=
 (continuous_pow n).comp h
 
-@[to_additive continuous_on_nsmul]
+@[to_additive]
 lemma continuous_on_pow {s : set M} (n : ℕ) : continuous_on (λ x, x ^ n) s :=
 (continuous_pow n).continuous_on
 
-@[to_additive continuous_at_nsmul]
+@[to_additive]
 lemma continuous_at_pow (x : M) (n : ℕ) : continuous_at (λ x, x ^ n) x :=
 (continuous_pow n).continuous_at
 

src/topology/continuous_function/algebra.lean

@@ -64,23 +64,23 @@ lemma coe_one [has_one β]  : ⇑(1 : C(α, β)) = 1 := rfl
 instance has_nsmul [add_monoid β] [has_continuous_add β] : has_scalar ℕ C(α, β) :=
 ⟨λ n f, ⟨n • f, f.continuous.nsmul n⟩⟩
 
-@[to_additive has_nsmul]
+@[to_additive]
 instance has_pow [monoid β] [has_continuous_mul β] : has_pow C(α, β) ℕ :=
 ⟨λ f n, ⟨f ^ n, f.continuous.pow n⟩⟩
 
-@[norm_cast, to_additive coe_nsmul]
+@[norm_cast, to_additive]
 lemma coe_pow [monoid β] [has_continuous_mul β] (f : C(α, β)) (n : ℕ) :
   ⇑(f ^ n) = f ^ n := rfl
-  
--- don't make `coe_nsmul` simp as the linter complains it's redundant WRT `coe_smul` 
+
+-- don't make `coe_nsmul` simp as the linter complains it's redundant WRT `coe_smul`
 attribute [simp] coe_pow
 
-@[to_additive nsmul_comp] lemma pow_comp [monoid γ] [has_continuous_mul γ]
+@[to_additive] lemma pow_comp [monoid γ] [has_continuous_mul γ]
   (f : C(β, γ)) (n : ℕ) (g : C(α, β)) :
   (f^n).comp g = (f.comp g)^n :=
 rfl
 
--- don't make `nsmul_comp` simp as the linter complains it's redundant WRT `smul_comp` 
+-- don't make `nsmul_comp` simp as the linter complains it's redundant WRT `smul_comp`
 attribute [simp] pow_comp
 
 @[to_additive]
@@ -122,15 +122,15 @@ lemma coe_zpow [group β] [topological_group β] (f : C(α, β)) (z : ℤ) :
   ⇑(f ^ z) = f ^ z :=
 rfl
 
--- don't make `coe_zsmul` simp as the linter complains it's redundant WRT `coe_smul` 
+-- don't make `coe_zsmul` simp as the linter complains it's redundant WRT `coe_smul`
 attribute [simp] coe_zpow
 
 @[to_additive]
 lemma zpow_comp [group γ] [topological_group γ] (f : C(β, γ)) (z : ℤ) (g : C(α, β)) :
   (f^z).comp g = (f.comp g)^z :=
 rfl
 
--- don't make `zsmul_comp` simp as the linter complains it's redundant WRT `smul_comp` 
+-- don't make `zsmul_comp` simp as the linter complains it's redundant WRT `smul_comp`
 attribute [simp] zpow_comp
 
 end continuous_map