From eb46e7e3cf98edd45bd1cce2227edb90d7e4426d Mon Sep 17 00:00:00 2001 From: Joachim Breitner Date: Mon, 7 Mar 2022 10:15:48 +0000 Subject: [PATCH] feat(algebra/group/to_additive): let to_additive turn `pow` into `nsmul` (#12477) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 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 | 2 +- src/algebra/big_operators/multiset.lean | 4 ++-- src/algebra/group/hom.lean | 2 +- src/algebra/group/pi.lean | 2 +- src/algebra/group/to_additive.lean | 1 + src/algebra/group_power/basic.lean | 12 ++++++------ src/algebra/group_power/order.lean | 6 +++--- src/algebra/iterate_hom.lean | 2 +- src/algebra/pointwise.lean | 4 ++-- src/group_theory/exponent.lean | 4 ++-- src/group_theory/order_of_element.lean | 14 +++++++------- src/group_theory/submonoid/membership.lean | 4 ++-- src/number_theory/divisors.lean | 2 +- src/topology/algebra/monoid.lean | 6 +++--- src/topology/continuous_function/algebra.lean | 16 ++++++++-------- 15 files changed, 41 insertions(+), 40 deletions(-) diff --git a/src/algebra/big_operators/basic.lean b/src/algebra/big_operators/basic.lean index 0e85b0e3d601a..2100e97bae1f5 100644 --- a/src/algebra/big_operators/basic.lean +++ b/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 diff --git a/src/algebra/big_operators/multiset.lean b/src/algebra/big_operators/multiset.lean index 29d9a2886166e..ef6c8014b3e64 100644 --- a/src/algebra/big_operators/multiset.lean +++ b/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 diff --git a/src/algebra/group/hom.lean b/src/algebra/group/hom.lean index 39019309d8879..027bf776079da 100644 --- a/src/algebra/group/hom.lean +++ b/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] diff --git a/src/algebra/group/pi.lean b/src/algebra/group/pi.lean index 2e5c1d2c7628b..206fcfd843a42 100644 --- a/src/algebra/group/pi.lean +++ b/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] diff --git a/src/algebra/group/to_additive.lean b/src/algebra/group/to_additive.lean index b9a680bda15a1..9f11b1bed3117 100644 --- a/src/algebra/group/to_additive.lean +++ b/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 diff --git a/src/algebra/group_power/basic.lean b/src/algebra/group_power/basic.lean index 80ef6e1995db3..74c03055fd763 100644 --- a/src/algebra/group_power/basic.lean +++ b/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 diff --git a/src/algebra/group_power/order.lean b/src/algebra/group_power/order.lean index ea4df89d71f84..9d5125e6143ac 100644 --- a/src/algebra/group_power/order.lean +++ b/src/algebra/group_power/order.lean @@ -81,7 +81,7 @@ 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 @@ -89,11 +89,11 @@ lemma pow_le_one_iff {x : M} {n : ℕ} (hn : n ≠ 0) : x ^ n ≤ 1 ↔ x ≤ 1 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] diff --git a/src/algebra/iterate_hom.lean b/src/algebra/iterate_hom.lean index 1c56297248b1c..f5bf0610a201e 100644 --- a/src/algebra/iterate_hom.lean +++ b/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) := diff --git a/src/algebra/pointwise.lean b/src/algebra/pointwise.lean index 2749052e0d2f0..08e38481fd92f 100644 --- a/src/algebra/pointwise.lean +++ b/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] diff --git a/src/group_theory/exponent.lean b/src/group_theory/exponent.lean index 513b10ab3d7d2..b042adb542108 100644 --- a/src/group_theory/exponent.lean +++ b/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 diff --git a/src/group_theory/order_of_element.lean b/src/group_theory/order_of_element.lean index 2e7a63fcf5bd3..06571d2160c5a 100644 --- a/src/group_theory/order_of_element.lean +++ b/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), diff --git a/src/group_theory/submonoid/membership.lean b/src/group_theory/submonoid/membership.lean index 1008973e6e592..4438386faddac 100644 --- a/src/group_theory/submonoid/membership.lean +++ b/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 diff --git a/src/number_theory/divisors.lean b/src/number_theory/divisors.lean index ce8259d18d372..c2fcf48645ec3 100644 --- a/src/number_theory/divisors.lean +++ b/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] diff --git a/src/topology/algebra/monoid.lean b/src/topology/algebra/monoid.lean index 4b35f696ca66b..636869c9e8253 100644 --- a/src/topology/algebra/monoid.lean +++ b/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 diff --git a/src/topology/continuous_function/algebra.lean b/src/topology/continuous_function/algebra.lean index 2ab9803d848f6..c6a2eb3125577 100644 --- a/src/topology/continuous_function/algebra.lean +++ b/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,7 +122,7 @@ 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] @@ -130,7 +130,7 @@ lemma zpow_comp [group γ] [topological_group γ] (f : C(β, γ)) (z : ℤ) (g : (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