feat(algebra/group_power/lemmas): Positivity of an odd/even power (#9796

)

This adds `odd.pow_nonneg` and co and `pow_right_comm`.
This also deletes `pow_odd_nonneg` and `pow_odd_pos` as they are special cases of `pow_nonneg` and `pow_pos`.
To make dot notation work, this renames `(pow/fpow)_(odd/even)_(nonneg/nonpos/pos/neg/abs)` to `(odd/even).(pow/fpow)_(nonneg/nonpos/pos/neg/abs)`

src/algebra/field_power.lean

@@ -28,7 +28,7 @@ f.to_ring_hom.map_fpow
   (-x) ^ (bit0 n) = x ^ bit0 n :=
 by rw [fpow_bit0', fpow_bit0', neg_mul_neg]
 
-lemma fpow_even_neg {K : Type*} [division_ring K] (a : K) {n : ℤ} (h : even n) :
+lemma even.fpow_neg {K : Type*} [division_ring K] {n : ℤ} (h : even n) (a : K) :
   (-a) ^ n = a ^ n :=
 begin
   obtain ⟨k, rfl⟩ := h,
@@ -135,52 +135,47 @@ end
 @[simp] theorem fpow_bit1_pos_iff : 0 < a ^ bit1 n ↔ 0 < a :=
 lt_iff_lt_of_le_iff_le fpow_bit1_nonpos_iff
 
-lemma fpow_even_nonneg (a : K) {n : ℤ} (hn : even n) :
+lemma even.fpow_nonneg {n : ℤ} (hn : even n) (a : K) :
   0 ≤ a ^ n :=
 begin
   cases le_or_lt 0 a with h h,
   { exact fpow_nonneg h _ },
-  { rw [←fpow_even_neg _ hn],
-    replace h : 0 ≤ -a := neg_nonneg_of_nonpos (le_of_lt h),
-    exact fpow_nonneg h _ }
+  { exact (hn.fpow_neg a).subst (fpow_nonneg (neg_nonneg_of_nonpos h.le) _) }
 end
 
-theorem fpow_even_pos (ha : a ≠ 0) (hn : even n) : 0 < a ^ n :=
+theorem even.fpow_pos (hn : even n) (ha : a ≠ 0) : 0 < a ^ n :=
 by cases hn with k hk; simpa only [hk, two_mul] using fpow_bit0_pos ha k
 
-theorem fpow_odd_nonneg (ha : 0 ≤ a) (hn : odd n) : 0 ≤ a ^ n :=
+theorem odd.fpow_nonneg (hn : odd n) (ha : 0 ≤ a) : 0 ≤ a ^ n :=
 by cases hn with k hk; simpa only [hk, two_mul] using fpow_bit1_nonneg_iff.mpr ha
 
-theorem fpow_odd_pos (ha : 0 < a) (hn : odd n) : 0 < a ^ n :=
+theorem odd.fpow_pos (hn : odd n) (ha : 0 < a) : 0 < a ^ n :=
 by cases hn with k hk; simpa only [hk, two_mul] using fpow_bit1_pos_iff.mpr ha
 
-theorem fpow_odd_nonpos (ha : a ≤ 0) (hn : odd n) : a ^ n ≤ 0:=
+theorem odd.fpow_nonpos (hn : odd n) (ha : a ≤ 0) : a ^ n ≤ 0:=
 by cases hn with k hk; simpa only [hk, two_mul] using fpow_bit1_nonpos_iff.mpr ha
 
-theorem fpow_odd_neg (ha : a < 0) (hn : odd n) : a ^ n < 0:=
+theorem odd.fpow_neg (hn : odd n) (ha : a < 0) : a ^ n < 0:=
 by cases hn with k hk; simpa only [hk, two_mul] using fpow_bit1_neg_iff.mpr ha
 
-lemma fpow_even_abs (a : K) {p : ℤ} (hp : even p) :
-  |a| ^ p = a ^ p :=
+lemma even.fpow_abs {p : ℤ} (hp : even p) (a : K) : |a| ^ p = a ^ p :=
 begin
   cases abs_choice a with h h;
-  simp only [h, fpow_even_neg _ hp],
+  simp only [h, hp.fpow_neg _],
 end
 
-@[simp] lemma fpow_bit0_abs (a : K) (p : ℤ) :
-  (|a|) ^ bit0 p = a ^ bit0 p :=
-fpow_even_abs _ (even_bit0 _)
+@[simp] lemma fpow_bit0_abs (a : K) (p : ℤ) : |a| ^ bit0 p = a ^ bit0 p :=
+(even_bit0 _).fpow_abs _
 
-lemma abs_fpow_even (a : K) {p : ℤ} (hp : even p) :
-  |a ^ p| = a ^ p :=
+lemma even.abs_fpow {p : ℤ} (hp : even p) (a : K) : |a ^ p| = a ^ p :=
 begin
   rw [abs_eq_self],
-  exact fpow_even_nonneg _ hp
+  exact hp.fpow_nonneg _
 end
 
 @[simp] lemma abs_fpow_bit0 (a : K) (p : ℤ) :
   |a ^ bit0 p| = a ^ bit0 p :=
-abs_fpow_even _ (even_bit0 _)
+(even_bit0 _).abs_fpow _
 
 end ordered_field_power
 

src/algebra/group_power/basic.lean

@@ -162,6 +162,10 @@ begin
   { rw [nat.mul_succ, pow_add, pow_succ', ih] }
 end
 
+@[to_additive nsmul_left_comm]
+lemma pow_right_comm (a : M) (m n : ℕ) : (a^m)^n = (a^n)^m :=
+by rw [←pow_mul, nat.mul_comm, pow_mul]
+
 @[to_additive mul_nsmul]
 theorem pow_mul' (a : M) (m n : ℕ) : a^(m * n) = (a^n)^m :=
 by rw [nat.mul_comm, pow_mul]

src/algebra/group_power/lemmas.lean

@@ -533,34 +533,40 @@ by simp only [le_iff_lt_or_eq, pow_bit1_neg_iff, pow_eq_zero_iff (bit1_pos (zero
 @[simp] theorem pow_bit1_pos_iff : 0 < a ^ bit1 n ↔ 0 < a :=
 lt_iff_lt_of_le_iff_le pow_bit1_nonpos_iff
 
-theorem pow_even_nonneg (a : R) (hn : even n) : 0 ≤ a ^ n :=
+lemma even.pow_nonneg (hn : even n) (a : R) : 0 ≤ a ^ n :=
 by cases hn with k hk; simpa only [hk, two_mul] using pow_bit0_nonneg a k
 
-theorem pow_even_pos (ha : a ≠ 0) (hn : even n) : 0 < a ^ n :=
+lemma even.pow_pos (hn : even n) (ha : a ≠ 0) : 0 < a ^ n :=
 by cases hn with k hk; simpa only [hk, two_mul] using pow_bit0_pos ha k
 
-theorem pow_odd_nonneg (ha : 0 ≤ a) (hn : odd n) : 0 ≤ a ^ n :=
-by cases hn with k hk; simpa only [hk, two_mul] using pow_bit1_nonneg_iff.mpr ha
-
-theorem pow_odd_pos (ha : 0 < a) (hn : odd n) : 0 < a ^ n :=
-by cases hn with k hk; simpa only [hk, two_mul] using pow_bit1_pos_iff.mpr ha
-
-theorem pow_odd_nonpos (ha : a ≤ 0) (hn : odd n) : a ^ n ≤ 0:=
+lemma odd.pow_nonpos (hn : odd n) (ha : a ≤ 0) : a ^ n ≤ 0:=
 by cases hn with k hk; simpa only [hk, two_mul] using pow_bit1_nonpos_iff.mpr ha
 
-theorem pow_odd_neg (ha : a < 0) (hn : odd n) : a ^ n < 0:=
+lemma odd.pow_neg (hn : odd n) (ha : a < 0) : a ^ n < 0:=
 by cases hn with k hk; simpa only [hk, two_mul] using pow_bit1_neg_iff.mpr ha
 
-lemma pow_even_abs (a : R) {p : ℕ} (hp : even p) :
-  |a| ^ p = a ^ p :=
+lemma odd.pow_nonneg_iff (hn : odd n) : 0 ≤ a ^ n ↔ 0 ≤ a :=
+⟨λ h, le_of_not_lt (λ ha, h.not_lt $ hn.pow_neg ha), λ ha, pow_nonneg ha n⟩
+
+lemma odd.pow_nonpos_iff (hn : odd n) : a ^ n ≤ 0 ↔ a ≤ 0 :=
+⟨λ h, le_of_not_lt (λ ha, h.not_lt $ pow_pos ha _), hn.pow_nonpos⟩
+
+lemma odd.pow_pos_iff (hn : odd n) : 0 < a ^ n ↔ 0 < a :=
+⟨λ h, lt_of_not_ge' (λ ha, h.not_le $ hn.pow_nonpos ha), λ ha, pow_pos ha n⟩
+
+lemma odd.pow_neg_iff (hn : odd n) : a ^ n < 0 ↔ a < 0 :=
+⟨λ h, lt_of_not_ge' (λ ha, h.not_le $ pow_nonneg ha _), hn.pow_neg⟩
+
+lemma even.pow_pos_iff (hn : even n) (h₀ : 0 < n) : 0 < a ^ n ↔ a ≠ 0 :=
+⟨λ h ha, by { rw [ha, zero_pow h₀] at h, exact lt_irrefl 0 h }, hn.pow_pos⟩
+
+lemma even.pow_abs {p : ℕ} (hp : even p) (a : R) : |a| ^ p = a ^ p :=
 begin
   rw [←abs_pow, abs_eq_self],
-  exact pow_even_nonneg _ hp
+  exact hp.pow_nonneg _
 end
 
-@[simp] lemma pow_bit0_abs (a : R) (p : ℕ) :
-  |a| ^ bit0 p = a ^ bit0 p :=
-pow_even_abs _ (even_bit0 _)
+@[simp] lemma pow_bit0_abs (a : R) (p : ℕ) : |a| ^ bit0 p = a ^ bit0 p := (even_bit0 _).pow_abs _
 
 lemma strict_mono_pow_bit1 (n : ℕ) : strict_mono (λ a : R, a ^ bit1 n) :=
 begin