refactor(algebra/group/to_additive + files containing even/odd): move many lemmas involving even/odd to the same file (#12882)

This is the first step in refactoring the definition of `even` to be the `to_additive` of `square`.

This PR simply gathers together many (though not all) lemmas that involve `even` or `odd` in their assumptions.  The choice of which lemmas to migrate to the file `algebra.parity` was dictated mostly by whether importing `algebra.parity` in the current home would create a cyclic import.

The only change that is not a simple shift from a file to another one is the addition in `to_additive` for support to change `square` in a multiplicative name to `even` in an additive name.

The change to the test file `test.ring` is due to the fact that the definition of `odd` was no longer imported by the file.

Author: adomani

src/algebra/field_power.lean

@@ -28,13 +28,6 @@ f.to_ring_hom.map_zpow
   (-x) ^ (bit0 n) = x ^ bit0 n :=
 by rw [zpow_bit0', zpow_bit0', neg_mul_neg]
 
-lemma even.zpow_neg {K : Type*} [division_ring K] {n : ℤ} (h : even n) (a : K) :
-  (-a) ^ n = a ^ n :=
-begin
-  obtain ⟨k, rfl⟩ := h,
-  rw [←bit0_eq_two_mul, zpow_bit0_neg],
-end
-
 @[simp] lemma zpow_bit1_neg {K : Type*} [division_ring K] (x : K) (n : ℤ) :
   (-x) ^ (bit1 n) = - x ^ bit1 n :=
 by rw [zpow_bit1', zpow_bit1', neg_mul_neg, neg_mul_eq_mul_neg]
@@ -135,48 +128,6 @@ end
 @[simp] theorem zpow_bit1_pos_iff : 0 < a ^ bit1 n ↔ 0 < a :=
 lt_iff_lt_of_le_iff_le zpow_bit1_nonpos_iff
 
-lemma even.zpow_nonneg {n : ℤ} (hn : even n) (a : K) :
-  0 ≤ a ^ n :=
-begin
-  cases le_or_lt 0 a with h h,
-  { exact zpow_nonneg h _ },
-  { exact (hn.zpow_neg a).subst (zpow_nonneg (neg_nonneg_of_nonpos h.le) _) }
-end
-
-theorem even.zpow_pos (hn : even n) (ha : a ≠ 0) : 0 < a ^ n :=
-by cases hn with k hk; simpa only [hk, two_mul] using zpow_bit0_pos ha k
-
-theorem odd.zpow_nonneg (hn : odd n) (ha : 0 ≤ a) : 0 ≤ a ^ n :=
-by cases hn with k hk; simpa only [hk, two_mul] using zpow_bit1_nonneg_iff.mpr ha
-
-theorem odd.zpow_pos (hn : odd n) (ha : 0 < a) : 0 < a ^ n :=
-by cases hn with k hk; simpa only [hk, two_mul] using zpow_bit1_pos_iff.mpr ha
-
-theorem odd.zpow_nonpos (hn : odd n) (ha : a ≤ 0) : a ^ n ≤ 0:=
-by cases hn with k hk; simpa only [hk, two_mul] using zpow_bit1_nonpos_iff.mpr ha
-
-theorem odd.zpow_neg (hn : odd n) (ha : a < 0) : a ^ n < 0:=
-by cases hn with k hk; simpa only [hk, two_mul] using zpow_bit1_neg_iff.mpr ha
-
-lemma even.zpow_abs {p : ℤ} (hp : even p) (a : K) : |a| ^ p = a ^ p :=
-begin
-  cases abs_choice a with h h;
-  simp only [h, hp.zpow_neg _],
-end
-
-@[simp] lemma zpow_bit0_abs (a : K) (p : ℤ) : |a| ^ bit0 p = a ^ bit0 p :=
-(even_bit0 _).zpow_abs _
-
-lemma even.abs_zpow {p : ℤ} (hp : even p) (a : K) : |a ^ p| = a ^ p :=
-begin
-  rw [abs_eq_self],
-  exact hp.zpow_nonneg _
-end
-
-@[simp] lemma abs_zpow_bit0 (a : K) (p : ℤ) :
-  |a ^ bit0 p| = a ^ bit0 p :=
-(even_bit0 _).abs_zpow _
-
 end ordered_field_power
 
 lemma one_lt_zpow {K} [linear_ordered_field K] {p : K} (hp : 1 < p) :

src/algebra/group/to_additive.lean

@@ -217,6 +217,7 @@ meta def tr : bool → list string → list string
 | 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 ("is" :: "square" :: s)             := add_comm_prefix is_comm "even"      :: tr ff s
 | is_comm ("monoid" :: s)      := ("add_" ++ add_comm_prefix is_comm "monoid")    :: tr ff s
 | is_comm ("submonoid" :: s)   := ("add_" ++ add_comm_prefix is_comm "submonoid") :: tr ff s
 | is_comm ("group" :: s)       := ("add_" ++ add_comm_prefix is_comm "group")     :: tr ff s

src/algebra/group_power/lemmas.lean

@@ -497,41 +497,6 @@ 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
 
-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
-
-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
-
-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
-
-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 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 hp.pow_nonneg _
-end
-
-@[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
   intros a b hab,
@@ -543,9 +508,6 @@ begin
   { exact pow_lt_pow_of_lt_left hab ha (bit1_pos (zero_le n)) }
 end
 
-lemma odd.strict_mono_pow (hn : odd n) : strict_mono (λ a : R, a ^ n) :=
-by cases hn with k hk; simpa only [hk, two_mul] using strict_mono_pow_bit1 _
-
 /-- Bernoulli's inequality for `n : ℕ`, `-2 ≤ a`. -/
 theorem one_add_mul_le_pow (H : -2 ≤ a) (n : ℕ) : 1 + (n : R) * a ≤ (1 + a) ^ n :=
 one_add_mul_le_pow' (mul_self_nonneg _) (mul_self_nonneg _) (neg_le_iff_add_nonneg'.1 H) _

src/algebra/order/ring.lean

@@ -1317,12 +1317,6 @@ lemma self_dvd_abs (a : α) : a ∣ |a| :=
 lemma abs_dvd_abs (a b : α) : |a| ∣ |b| ↔ a ∣ b :=
 (abs_dvd _ _).trans (dvd_abs _ _)
 
-lemma even_abs {a : α} : even (|a|) ↔ even a :=
-dvd_abs _ _
-
-lemma odd_abs {a : α} : odd (abs a) ↔ odd a :=
-by { cases abs_choice a with h h; simp only [h, odd_neg] }
-
 end
 
 section linear_ordered_comm_ring