feat(algebra/group_power/lemmas): More lemmas through to_additive (#…

…13537)

Use `to_additive` to generate a bunch of old `nsmul`/`zsmul` lemmas from new `pow`/`zpow` ones. Also protect `nat.nsmul_eq_mul` as it should have been.

src/algebra/group_power/basic.lean

@@ -452,7 +452,8 @@ lemma of_mul_zpow [div_inv_monoid G] (x : G) (n : ℤ) :
   additive.of_mul (x ^ n) = n • additive.of_mul x :=
 rfl
 
-@[simp] lemma semiconj_by.zpow_right [group G] {a x y : G} (h : semiconj_by a x y) :
+@[simp, to_additive]
+lemma semiconj_by.zpow_right [group G] {a x y : G} (h : semiconj_by a x y) :
   ∀ m : ℤ, semiconj_by a (x^m) (y^m)
 | (n : ℕ) := by simp [zpow_coe_nat, h.pow_right n]
 | -[1+n] := by simp [(h.pow_right n.succ).inv_right]
@@ -461,18 +462,19 @@ namespace commute
 
 variables [group G] {a b : G}
 
-@[simp] lemma zpow_right (h : commute a b) (m : ℤ) : commute a (b^m) :=
-h.zpow_right m
+@[simp, to_additive] lemma zpow_right (h : commute a b) (m : ℤ) : commute a (b^m) := h.zpow_right m
 
-@[simp] lemma zpow_left (h : commute a b) (m : ℤ) : commute (a^m) b :=
+@[simp, to_additive] lemma zpow_left (h : commute a b) (m : ℤ) : commute (a^m) b :=
 (h.symm.zpow_right m).symm
 
+@[to_additive]
 lemma zpow_zpow (h : commute a b) (m n : ℤ) : commute (a^m) (b^n) := (h.zpow_left m).zpow_right n
 
 variables (a) (m n : ℤ)
 
-@[simp] theorem self_zpow : commute a (a ^ n) := (commute.refl a).zpow_right n
-@[simp] theorem zpow_self : commute (a ^ n) a := (commute.refl a).zpow_left n
-@[simp] theorem zpow_zpow_self : commute (a ^ m) (a ^ n) := (commute.refl a).zpow_zpow m n
+@[simp, to_additive] lemma self_zpow : commute a (a ^ n) := (commute.refl a).zpow_right n
+@[simp, to_additive] lemma zpow_self : commute (a ^ n) a := (commute.refl a).zpow_left n
+@[simp, to_additive] lemma zpow_zpow_self : commute (a ^ m) (a ^ n) :=
+(commute.refl a).zpow_zpow m n
 
 end commute

src/algebra/group_power/lemmas.lean

@@ -13,9 +13,11 @@ This file contains lemmas about `monoid.pow`, `group.pow`, `nsmul`, `zsmul`
 which require additional imports besides those available in `algebra.group_power.basic`.
 -/
 
+open function int nat
+
 universes u v w x y z u₁ u₂
 
-variables {M : Type u} {N : Type v} {G : Type w} {H : Type x} {A : Type y} {B : Type z}
+variables {α : Type*} {M : Type u} {N : Type v} {G : Type w} {H : Type x} {A : Type y} {B : Type z}
   {R : Type u₁} {S : Type u₂}
 
 /-!
@@ -96,16 +98,15 @@ end
 
 end monoid
 
-section group
-variables [group G] [group H] [add_group A] [add_group B]
+section sub_neg_monoid
+variables [sub_neg_monoid A]
 
-open int
+lemma zsmul_one [has_one A] (n : ℤ) : n • (1 : A) = n := by cases n; simp
 
-local attribute [ematch] le_of_lt
-open nat
+end sub_neg_monoid
 
-theorem zsmul_one [has_one A] (n : ℤ) : n • (1 : A) = n :=
-by cases n; simp
+section group
+variables [group G]
 
 @[to_additive add_one_zsmul]
 lemma zpow_add_one (a : G) : ∀ n : ℤ, a ^ (n + 1) = a ^ n * a
@@ -168,73 +169,107 @@ by rw [bit1, zpow_add, zpow_bit0, zpow_one]
 
 end group
 
-section ordered_add_comm_group
+/-!
+### `zpow`/`zsmul` and an order
 
-variables [ordered_add_comm_group A]
-/-! Lemmas about `zsmul` under ordering,  placed here (rather than in `algebra.group_power.order`
-with their friends) because they require facts from `data.int.basic`-/
-open int
+Those lemmas are placed here (rather than in `algebra.group_power.order` with their friends) because
+they require facts from `data.int.basic`.
+-/
 
-lemma zsmul_pos {a : A} (ha : 0 < a) {k : ℤ} (hk : (0:ℤ) < k) : 0 < k • a :=
+section ordered_add_comm_group
+variables [ordered_comm_group α] {m n : ℤ} {a b : α}
+
+@[to_additive zsmul_pos]
+lemma one_lt_zpow' (ha : 1 < a) {k : ℤ} (hk : (0:ℤ) < k) : 1 < a^k :=
 begin
   lift k to ℕ using int.le_of_lt hk,
-  rw coe_nat_zsmul,
-  apply nsmul_pos ha,
-  exact (coe_nat_pos.mp hk).ne',
+  rw zpow_coe_nat,
+  exact one_lt_pow' ha (coe_nat_pos.mp hk).ne',
 end
 
-theorem zsmul_strict_mono_left {a : A} (ha : 0 < a) : strict_mono (λ n : ℤ, n • a) :=
-λ n m h,
-  calc n • a = n • a + 0 : (add_zero _).symm
-    ... < n • a + (m - n) • a : add_lt_add_left (zsmul_pos ha (sub_pos.mpr h)) _
-    ... = m • a : by { rw [← add_zsmul], simp }
+@[to_additive zsmul_strict_mono_left]
+lemma zpow_strict_mono_right (ha : 1 < a) : strict_mono (λ n : ℤ, a ^ n) :=
+λ m n h,
+  calc a ^ m = a ^ m * 1 : (mul_one _).symm
+    ... < a ^ m * a ^ (n - m) : mul_lt_mul_left' (one_lt_zpow' ha $ sub_pos_of_lt h) _
+    ... = a ^ n : by { rw ←zpow_add, simp }
 
-theorem zsmul_mono_left {a : A} (ha : 0 ≤ a) : monotone (λ n : ℤ, n • a) :=
-λ n m h,
-  calc n • a = n • a + 0 : (add_zero _).symm
-    ... ≤ n • a + (m - n) • a : add_le_add_left (zsmul_nonneg ha (sub_nonneg.mpr h)) _
-    ... = m • a : by { rw [← add_zsmul], simp }
+@[to_additive zsmul_mono_left]
+lemma zpow_mono_right (ha : 1 ≤ a) : monotone (λ n : ℤ, a ^ n) :=
+λ m n h,
+  calc a ^ m = a ^ m * 1 : (mul_one _).symm
+    ... ≤ a ^ m * a ^ (n - m) : mul_le_mul_left' (one_le_zpow ha $ sub_nonneg_of_le h) _
+    ... = a ^ n : by { rw ←zpow_add, simp }
 
-theorem zsmul_le_zsmul {a : A} {n m : ℤ} (ha : 0 ≤ a) (h : n ≤ m) : n • a ≤ m • a :=
-zsmul_mono_left ha h
+@[to_additive]
+lemma zpow_le_zpow (ha : 1 ≤ a) (h : m ≤ n) : a ^ m ≤ a ^ n := zpow_mono_right ha h
 
-theorem zsmul_lt_zsmul {a : A} {n m : ℤ} (ha : 0 < a) (h : n < m) : n • a < m • a :=
-zsmul_strict_mono_left ha h
+@[to_additive]
+lemma zpow_lt_zpow (ha : 1 < a) (h : m < n) : a ^ m < a ^ n := zpow_strict_mono_right ha h
 
-theorem zsmul_le_zsmul_iff {a : A} {n m : ℤ} (ha : 0 < a) : n • a ≤ m • a ↔ n ≤ m :=
-(zsmul_strict_mono_left ha).le_iff_le
+@[to_additive]
+lemma zpow_le_zpow_iff (ha : 1 < a) : a ^ m ≤ a ^ n ↔ m ≤ n := (zpow_strict_mono_right ha).le_iff_le
 
-theorem zsmul_lt_zsmul_iff {a : A} {n m : ℤ} (ha : 0 < a) : n • a < m • a ↔ n < m :=
-(zsmul_strict_mono_left ha).lt_iff_lt
+@[to_additive]
+lemma zpow_lt_zpow_iff (ha : 1 < a) : a ^ m < a ^ n ↔ m < n := (zpow_strict_mono_right ha).lt_iff_lt
 
-variables (A)
+variables (α)
 
-lemma zsmul_strict_mono_right {n : ℤ} (hn : 0 < n) :
-  strict_mono ((•) n : A → A) :=
-λ a b hab, begin
-  rw ← sub_pos at hab,
-  rw [← sub_pos, ← zsmul_sub],
-  exact zsmul_pos hab hn,
-end
+@[to_additive zsmul_strict_mono_right]
+lemma zpow_strict_mono_left (hn : 0 < n) : strict_mono ((^ n) : α → α) :=
+λ a b hab, by { rw [←one_lt_div', ←div_zpow], exact one_lt_zpow' (one_lt_div'.2 hab) hn }
+
+@[to_additive zsmul_mono_right]
+lemma zpow_mono_left (hn : 0 ≤ n) : monotone ((^ n) : α → α) :=
+λ a b hab, by { rw [←one_le_div', ←div_zpow], exact one_le_zpow (one_le_div'.2 hab) hn }
+
+variables {α}
+
+@[to_additive]
+lemma zpow_le_zpow' (hn : 0 ≤ n) (h : a ≤ b) : a ^ n ≤ b ^ n := zpow_mono_left α hn h
+
+@[to_additive]
+lemma zpow_lt_zpow' (hn : 0 < n) (h : a < b) : a ^ n < b ^ n := zpow_strict_mono_left α hn h
+
+end ordered_add_comm_group
+
+section linear_ordered_comm_group
+variables [linear_ordered_comm_group α] {n : ℤ} {a b : α}
+
+@[to_additive]
+lemma zpow_le_zpow_iff' (hn : 0 < n) {a b : α} : a ^ n ≤ b ^ n ↔ a ≤ b :=
+(zpow_strict_mono_left α hn).le_iff_le
+
+@[to_additive]
+lemma zpow_lt_zpow_iff' (hn : 0 < n) {a b : α} : a ^ n < b ^ n ↔ a < b :=
+(zpow_strict_mono_left α hn).lt_iff_lt
 
-lemma zsmul_mono_right {n : ℤ} (hn : 0 ≤ n) :
-  monotone ((•) n : A → A) :=
-λ a b hab, begin
-  rw ← sub_nonneg at hab,
-  rw [← sub_nonneg, ← zsmul_sub],
-  exact zsmul_nonneg hab hn,
+@[nolint to_additive_doc, to_additive zsmul_right_injective
+"See also `smul_right_injective`. TODO: provide a `no_zero_smul_divisors` instance. We can't do that
+here because importing that definition would create import cycles."]
+lemma zpow_left_injective (hn : n ≠ 0) : function.injective ((^ n) : α → α) :=
+begin
+  cases hn.symm.lt_or_lt,
+  { exact (zpow_strict_mono_left α h).injective },
+  { refine λ a b (hab : a ^ n = b ^ n), (zpow_strict_mono_left α (neg_pos.mpr h)).injective _,
+    rw [zpow_neg, zpow_neg, hab] }
 end
 
-variables {A}
+@[to_additive zsmul_right_inj]
+lemma zpow_left_inj (hn : n ≠ 0) : a ^ n = b ^ n ↔ a = b := (zpow_left_injective hn).eq_iff
 
-theorem zsmul_le_zsmul' {n : ℤ} (hn : 0 ≤ n) {a₁ a₂ : A} (h : a₁ ≤ a₂) : n • a₁ ≤ n • a₂ :=
-zsmul_mono_right A hn h
+/-- Alias of `zsmul_right_inj`, for ease of discovery alongside `zsmul_le_zsmul_iff'` and
+`zsmul_lt_zsmul_iff'`. -/
+@[to_additive "Alias of `zsmul_right_inj`, for ease of discovery alongside `zsmul_le_zsmul_iff'` and
+`zsmul_lt_zsmul_iff'`."]
+lemma zpow_eq_zpow_iff' (hn : n ≠ 0) : a ^ n = b ^ n ↔ a = b := zpow_left_inj hn
 
-theorem zsmul_lt_zsmul' {n : ℤ} (hn : 0 < n) {a₁ a₂ : A} (h : a₁ < a₂) : n • a₁ < n • a₂ :=
-zsmul_strict_mono_right A hn h
+end linear_ordered_comm_group
 
-lemma abs_nsmul {α : Type*} [linear_ordered_add_comm_group α] (n : ℕ) (a : α) :
-  |n • a| = n • |a| :=
+section linear_ordered_add_comm_group
+variables [linear_ordered_add_comm_group α] {a b : α}
+
+lemma abs_nsmul (n : ℕ) (a : α) : |n • a| = n • |a| :=
 begin
   cases le_total a 0 with hneg hpos,
   { rw [abs_of_nonpos hneg, ← abs_neg, ← neg_nsmul, abs_of_nonneg],
@@ -243,91 +278,42 @@ begin
     exact nsmul_nonneg hpos n }
 end
 
-lemma abs_zsmul {α : Type*} [linear_ordered_add_comm_group α] (n : ℤ) (a : α) :
-  |n • a| = |n| • |a| :=
+lemma abs_zsmul (n : ℤ) (a : α) : |n • a| = |n| • |a| :=
 begin
-  by_cases n0 : 0 ≤ n,
+  obtain n0 | n0 := le_total 0 n,
   { lift n to ℕ using n0,
     simp only [abs_nsmul, coe_nat_abs, coe_nat_zsmul] },
-  { lift (- n) to ℕ using int.le_of_lt (neg_pos.mpr (not_le.mp n0)) with m h,
+  { lift (- n) to ℕ using neg_nonneg.2 n0 with m h,
     rw [← abs_neg (n • a), ← neg_zsmul, ← abs_neg n, ← h, coe_nat_zsmul, coe_nat_abs,
       coe_nat_zsmul],
     exact abs_nsmul m _ },
 end
 
-lemma abs_add_eq_add_abs_le {α : Type*} [linear_ordered_add_comm_group α] {a b : α} (hle : a ≤ b) :
-  |a + b| = |a| + |b| ↔ (0 ≤ a ∧ 0 ≤ b ∨ a ≤ 0 ∧ b ≤ 0) :=
+lemma abs_add_eq_add_abs_le (hle : a ≤ b) : |a + b| = |a| + |b| ↔ 0 ≤ a ∧ 0 ≤ b ∨ a ≤ 0 ∧ b ≤ 0 :=
 begin
-  by_cases a0 : 0 ≤ a; by_cases b0 : 0 ≤ b,
+  obtain a0 | a0 := le_or_lt 0 a; obtain b0 | b0 := le_or_lt 0 b,
   { simp [a0, b0, abs_of_nonneg, add_nonneg a0 b0] },
-  { exact (lt_irrefl (0 : α) (a0.trans_lt (hle.trans_lt (not_le.mp b0)))).elim },
-  any_goals { simp [(not_le.mp a0).le, (not_le.mp b0).le, abs_of_nonpos, add_nonpos, add_comm] },
-  obtain F := (not_le.mp a0),
+  { exact (lt_irrefl (0 : α) $ a0.trans_lt $ hle.trans_lt b0).elim },
+  any_goals { simp [a0.le, b0.le, abs_of_nonpos, add_nonpos, add_comm] },
   have : (|a + b| = -a + b ↔ b ≤ 0) ↔ (|a + b| =
     |a| + |b| ↔ 0 ≤ a ∧ 0 ≤ b ∨ a ≤ 0 ∧ b ≤ 0),
-  { simp [a0, b0, abs_of_neg, abs_of_nonneg, F, F.le] },
-  refine this.mp ⟨λ h, _, λ h, by simp only [le_antisymm h b0, abs_of_neg F, add_zero]⟩,
-  by_cases ba : a + b ≤ 0,
+  { simp [a0, a0.le, a0.not_le, b0, abs_of_neg, abs_of_nonneg] },
+  refine this.mp ⟨λ h, _, λ h, by simp only [le_antisymm h b0, abs_of_neg a0, add_zero]⟩,
+  obtain ab | ab := le_or_lt (a + b) 0,
   { refine le_of_eq (eq_zero_of_neg_eq _),
-    rwa [abs_of_nonpos ba, neg_add_rev, add_comm, add_right_inj] at h },
+    rwa [abs_of_nonpos ab, neg_add_rev, add_comm, add_right_inj] at h },
   { refine (lt_irrefl (0 : α) _).elim,
-    rw [abs_of_pos (not_le.mp ba), add_left_inj] at h,
-    rwa eq_zero_of_neg_eq h.symm at F }
+    rw [abs_of_pos ab, add_left_inj] at h,
+    rwa eq_zero_of_neg_eq h.symm at a0 }
 end
 
-lemma abs_add_eq_add_abs_iff {α : Type*} [linear_ordered_add_comm_group α] (a b : α) :
-  |a + b| = |a| + |b| ↔ (0 ≤ a ∧ 0 ≤ b ∨ a ≤ 0 ∧ b ≤ 0) :=
+lemma abs_add_eq_add_abs_iff (a b : α) : |a + b| = |a| + |b| ↔ 0 ≤ a ∧ 0 ≤ b ∨ a ≤ 0 ∧ b ≤ 0 :=
 begin
-  by_cases ab : a ≤ b,
+  obtain ab | ab := le_total a b,
   { exact abs_add_eq_add_abs_le ab },
-  { rw [add_comm a, add_comm (abs _), abs_add_eq_add_abs_le ((not_le.mp ab).le), and.comm,
-    @and.comm (b ≤ 0 ) _] }
+  { rw [add_comm a, add_comm (abs _), abs_add_eq_add_abs_le ab, and.comm, @and.comm (b ≤ 0)] }
 end
 
-end ordered_add_comm_group
-
-section linear_ordered_add_comm_group
-variable [linear_ordered_add_comm_group A]
-
-theorem zsmul_le_zsmul_iff' {n : ℤ} (hn : 0 < n) {a₁ a₂ : A} : n • a₁ ≤ n • a₂ ↔ a₁ ≤ a₂ :=
-(zsmul_strict_mono_right A hn).le_iff_le
-
-theorem zsmul_lt_zsmul_iff' {n : ℤ} (hn : 0 < n) {a₁ a₂ : A} : n • a₁ < n • a₂ ↔ a₁ < a₂ :=
-(zsmul_strict_mono_right A hn).lt_iff_lt
-
-theorem nsmul_le_nsmul_iff {a : A} {n m : ℕ} (ha : 0 < a) : n • a ≤ m • a ↔ n ≤ m :=
-begin
-  refine ⟨λ h, _, nsmul_le_nsmul $ le_of_lt ha⟩,
-  by_contra H,
-  exact lt_irrefl _ (lt_of_lt_of_le (nsmul_lt_nsmul ha (not_le.mp H)) h)
-end
-
-theorem nsmul_lt_nsmul_iff {a : A} {n m : ℕ} (ha : 0 < a) : n • a < m • a ↔ n < m :=
-begin
-  refine ⟨λ h, _, nsmul_lt_nsmul ha⟩,
-  by_contra H,
-  exact lt_irrefl _ (lt_of_le_of_lt (nsmul_le_nsmul (le_of_lt ha) $ not_lt.mp H) h)
-end
-
-/-- See also `smul_right_injective`. TODO: provide a `no_zero_smul_divisors` instance. We can't
-do that here because importing that definition would create import cycles. -/
-lemma zsmul_right_injective {m : ℤ} (hm : m ≠ 0) : function.injective ((•) m : A → A) :=
-begin
-  cases hm.symm.lt_or_lt,
-  { exact (zsmul_strict_mono_right A h).injective, },
-  { intros a b hab,
-    refine (zsmul_strict_mono_right A (neg_pos.mpr h)).injective _,
-    rw [neg_zsmul, neg_zsmul, hab], },
-end
-
-lemma zsmul_right_inj {a b : A} {m : ℤ} (hm : m ≠ 0) : m • a = m • b ↔ a = b :=
-(zsmul_right_injective hm).eq_iff
-
-/-- Alias of `zsmul_right_inj`, for ease of discovery alongside `zsmul_le_zsmul_iff'` and
-`zsmul_lt_zsmul_iff'`. -/
-lemma zsmul_eq_zsmul_iff' {a b : A} {m : ℤ} (hm : m ≠ 0) : m • a = m • b ↔ a = b :=
-zsmul_right_inj hm
-
 end linear_ordered_add_comm_group
 
 @[simp] lemma with_bot.coe_nsmul [add_monoid A] (a : A) (n : ℕ) :
@@ -774,16 +760,16 @@ h.cast_nat_mul_right n
 h.cast_nat_mul_left n
 
 @[simp] theorem cast_nat_mul_cast_nat_mul (h : commute a b) (m n : ℕ) :
-  commute ((m : R) * a) (n * b) :=
+  commute (m * a : R) (n * b : R) :=
 h.cast_nat_mul_cast_nat_mul m n
 
-@[simp] theorem self_cast_nat_mul (n : ℕ) : commute a (n * a) :=
+@[simp] theorem self_cast_nat_mul (n : ℕ) : commute a (n * a : R) :=
 (commute.refl a).cast_nat_mul_right n
 
 @[simp] theorem cast_nat_mul_self (n : ℕ) : commute ((n : R) * a) a :=
 (commute.refl a).cast_nat_mul_left n
 
-@[simp] theorem self_cast_nat_mul_cast_nat_mul (m n : ℕ) : commute ((m : R) * a) (n * a) :=
+@[simp] theorem self_cast_nat_mul_cast_nat_mul (m n : ℕ) : commute (m * a : R) (n * a : R) :=
 (commute.refl a).cast_nat_mul_cast_nat_mul m n
 
 end
@@ -800,13 +786,13 @@ h.units_zpow_right m
 
 variables {a b : R}
 
-@[simp] lemma cast_int_mul_right (h : commute a b) (m : ℤ) : commute a (m * b) :=
+@[simp] lemma cast_int_mul_right (h : commute a b) (m : ℤ) : commute a (m * b : R) :=
 h.cast_int_mul_right m
 
 @[simp] lemma cast_int_mul_left (h : commute a b) (m : ℤ) : commute ((m : R) * a) b :=
 h.cast_int_mul_left m
 
-lemma cast_int_mul_cast_int_mul (h : commute a b) (m n : ℤ) : commute ((m : R) * a) (n * b) :=
+lemma cast_int_mul_cast_int_mul (h : commute a b) (m n : ℤ) : commute (m * a : R) (n * b : R) :=
 h.cast_int_mul_cast_int_mul m n
 
 variables (a) (m n : ℤ)
@@ -817,11 +803,11 @@ by { rw [← mul_one (m : R)], exact (one_left a).cast_int_mul_left m }
 @[simp] lemma cast_int_right : commute a m :=
 by { rw [← mul_one (m : R)], exact (one_right a).cast_int_mul_right m }
 
-@[simp] theorem self_cast_int_mul : commute a (n * a) := (commute.refl a).cast_int_mul_right n
+@[simp] theorem self_cast_int_mul : commute a (n * a : R) := (commute.refl a).cast_int_mul_right n
 
 @[simp] theorem cast_int_mul_self : commute ((n : R) * a) a := (commute.refl a).cast_int_mul_left n
 
-theorem self_cast_int_mul_cast_int_mul : commute ((m : R) * a) (n * a) :=
+theorem self_cast_int_mul_cast_int_mul : commute (m * a : R) (n * a : R) :=
 (commute.refl a).cast_int_mul_cast_int_mul m n
 
 end commute