feat(algebra/parity + *): generalize lemmas about parity (#12761)

I moved more even/odd lemmas from nat/int to general semirings/rings.

Some files that explicitly used the nat/int namespace were changed along the way.

src/algebra/geom_sum.lean

@@ -429,7 +429,7 @@ lemma geom_sum_alternating_of_lt_neg_one [ordered_ring α] (hx : x + 1 < 0) (hn
 begin
   have hx0 : x < 0, from ((le_add_iff_nonneg_right _).2 (@zero_le_one α _)).trans_lt hx,
   refine nat.le_induction _ _ n (show 2 ≤ n, from hn),
-  { simp only [geom_sum_two, hx, true_or, nat.even_bit0, if_true_left_eq_or] },
+  { simp only [geom_sum_two, hx, true_or, even_bit0, if_true_left_eq_or] },
   clear hn n,
   intros n hn ihn,
   simp only [nat.even_succ, geom_sum_succ],

src/algebra/parity.lean

@@ -5,36 +5,34 @@ Authors: Damiano Testa
 -/
 
 import algebra.ring.basic
+import algebra.algebra.basic
+import algebra.group_power.basic
 
 /-!  This file proves some general facts about even and odd elements of semirings. -/
 
-variables {α : Type*}
+variables {α β : Type*}
 
 section semiring
-variable [semiring α]
+variables [semiring α] [semiring β] {m n : α}
 
-theorem even.add_even {m n : α} (hm : even m) (hn : even n) :
-  even (m + n) :=
+lemma even.add_even (hm : even m) (hn : even n) : even (m + n) :=
 begin
   rcases hm with ⟨m, rfl⟩,
   rcases hn with ⟨n, rfl⟩,
   exact ⟨m + n, (mul_add _ _ _).symm⟩
 end
 
-theorem even.add_odd {m n : α} (hm : even m) (hn : odd n) :
-  odd (m + n) :=
+lemma even.add_odd (hm : even m) (hn : odd n) : odd (m + n) :=
 begin
   rcases hm with ⟨m, rfl⟩,
   rcases hn with ⟨n, rfl⟩,
   exact ⟨m + n, by rw [mul_add, add_assoc]⟩
 end
 
-theorem odd.add_even {m n : α} (hm : odd m) (hn : even n) :
-  odd (m + n) :=
+lemma odd.add_even (hm : odd m) (hn : even n) : odd (m + n) :=
 by { rw add_comm, exact hn.add_odd hm }
 
-theorem odd.add_odd {m n : α} (hm : odd m) (hn : odd n) :
-  even (m + n) :=
+lemma odd.add_odd (hm : odd m) (hn : odd n) : even (m + n) :=
 begin
   rcases hm with ⟨m, rfl⟩,
   rcases hn with ⟨n, rfl⟩,
@@ -43,4 +41,71 @@ begin
   refl
 end
 
+@[simp] lemma even_zero : even (0 : α) := ⟨0, (mul_zero _).symm⟩
+
+@[simp] lemma odd_one : odd (1 : α) :=
+⟨0, (zero_add _).symm.trans (congr_arg (+ (1 : α)) (mul_zero _).symm)⟩
+
+@[simp] lemma even_two : even (2 : α) := ⟨1, (mul_one _).symm⟩
+
+lemma even_two_mul (m : α) : even (2 * m) := ⟨m, rfl⟩
+
+@[simp] lemma odd_two_mul_add_one (m : α) : odd (2 * m + 1) := ⟨m, rfl⟩
+
+lemma add_monoid_hom.even (f : α →+ β) (hm : even m) : even (f m) :=
+begin
+  rcases hm with ⟨m, rfl⟩,
+  exact ⟨f m, by simp [two_mul]⟩
+end
+
+lemma ring_hom.odd (f : α →+* β) (hm : odd m) : odd (f m) :=
+begin
+  rcases hm with ⟨m, rfl⟩,
+  exact ⟨f m, by simp [two_mul]⟩
+end
+
+@[simp] lemma even.mul_right (hm : even m) (n) : even (m * n) :=
+(add_monoid_hom.mul_right n).even hm
+
+@[simp] lemma even.mul_left (hm : even m) (n) : even (n * m) :=
+(add_monoid_hom.mul_left n).even hm
+
+@[simp] lemma odd.mul_odd (hm : odd m) (hn : odd n) : odd (m * n) :=
+begin
+  rcases hm with ⟨m, rfl⟩,
+  rcases hn with ⟨n, rfl⟩,
+  refine ⟨2 * m * n + n + m, _⟩,
+  rw [mul_add, add_mul, mul_one, ← add_assoc, one_mul, mul_assoc, ← mul_add, ← mul_add, ← mul_assoc,
+    ← nat.cast_two, ← nat.cast_comm],
+end
+
+lemma even.pow_of_ne_zero (hm : even m) : ∀ {a : ℕ}, a ≠ 0 → even (m ^ a)
+| 0       a0 := (a0 rfl).elim
+| (a + 1) _  := by { rw pow_succ, exact hm.mul_right _ }
+
+lemma odd.pow (hm : odd m) : ∀ {a : ℕ}, odd (m ^ a)
+| 0       := by { rw pow_zero, exact odd_one }
+| (a + 1) := by { rw pow_succ, exact hm.mul_odd odd.pow }
+
 end semiring
+
+section ring
+variables [ring α] {m n : α}
+
+@[simp] lemma odd_neg_one : odd (- 1 : α) := by simp
+
+@[simp] lemma even_neg_two : even (- 2 : α) := by simp
+
+lemma even.sub_even (hm : even m) (hn : even n) : even (m - n) :=
+by { rw sub_eq_add_neg, exact hm.add_even ((even_neg n).mpr hn) }
+
+theorem odd.sub_even (hm : odd m) (hn : even n) : odd (m - n) :=
+by { rw sub_eq_add_neg, exact hm.add_even ((even_neg n).mpr hn) }
+
+theorem even.sub_odd (hm : even m) (hn : odd n) : odd (m - n) :=
+by { rw sub_eq_add_neg, exact hm.add_odd ((odd_neg n).mpr hn) }
+
+lemma odd.sub_odd (hm : odd m) (hn : odd n) : even (m - n) :=
+by { rw sub_eq_add_neg, exact hm.add_odd ((odd_neg n).mpr hn) }
+
+end ring

src/analysis/convex/specific_functions.lean

@@ -53,7 +53,7 @@ begin
   apply convex_on_univ_of_deriv2_nonneg differentiable_pow,
   { simp only [deriv_pow', differentiable.mul, differentiable_const, differentiable_pow] },
   { intro x,
-    rcases nat.even.sub_even hn (nat.even_bit0 1) with ⟨k, hk⟩,
+    rcases nat.even.sub_even hn (even_bit0 1) with ⟨k, hk⟩,
     rw [iter_deriv_pow, finset.prod_range_cast_nat_sub, hk, pow_mul'],
     exact mul_nonneg (nat.cast_nonneg _) (pow_two_nonneg _) }
 end
@@ -138,7 +138,7 @@ begin
   { intros x hx,
     simp only [iter_deriv_zpow, ← int.cast_coe_nat, ← int.cast_sub, ← int.cast_prod],
     refine mul_nonneg (int.cast_nonneg.2 _) (zpow_nonneg (le_of_lt hx) _),
-    exact int_prod_range_nonneg _ _ (nat.even_bit0 1) }
+    exact int_prod_range_nonneg _ _ (even_bit0 1) }
 end
 
 /-- `x^m`, `m : ℤ` is convex on `(0, +∞)` for all `m` except `0` and `1`. -/
@@ -154,7 +154,7 @@ begin
   intros x hx,
   simp only [iter_deriv_zpow, ← int.cast_coe_nat, ← int.cast_sub, ← int.cast_prod],
   refine mul_pos (int.cast_pos.2 _) (zpow_pos_of_pos hx _),
-  refine int_prod_range_pos (nat.even_bit0 1) (λ hm, _),
+  refine int_prod_range_pos (even_bit0 1) (λ hm, _),
   norm_cast at hm,
   rw ←finset.coe_Ico at hm,
   fin_cases hm,

src/data/int/parity.lean

@@ -80,14 +80,9 @@ instance : decidable_pred (even : ℤ → Prop) :=
 instance decidable_pred_odd : decidable_pred (odd : ℤ → Prop) :=
 λ n, decidable_of_decidable_of_iff (by apply_instance) odd_iff_not_even.symm
 
-@[simp] theorem even_zero : even (0 : ℤ) := ⟨0, dec_trivial⟩
-
 @[simp] theorem not_even_one : ¬ even (1 : ℤ) :=
 by rw even_iff; norm_num
 
-@[simp] theorem even_bit0 (n : ℤ) : even (bit0 n) :=
-⟨n, by rw [bit0, two_mul]⟩
-
 @[parity_simps] theorem even_add : even (m + n) ↔ (even m ↔ even n) :=
 by cases mod_two_eq_zero_or_one m with h₁ h₁;
    cases mod_two_eq_zero_or_one n with h₂ h₂;
@@ -106,15 +101,9 @@ by convert not_even_bit1 n; exact two_mul n
 @[parity_simps] theorem even_sub : even (m - n) ↔ (even m ↔ even n) :=
 by simp [sub_eq_add_neg] with parity_simps
 
-theorem even.sub_even (hm : even m) (hn : even n) : even (m - n) :=
-even_sub.2 $ iff_of_true hm hn
-
 theorem even_sub' : even (m - n) ↔ (odd m ↔ odd n) :=
 by rw [even_sub, even_iff_not_odd, even_iff_not_odd, not_iff_not]
 
-theorem odd.sub_odd (hm : odd m) (hn : odd n) : even (m - n) :=
-even_sub'.2 $ iff_of_true hm hn
-
 @[parity_simps] theorem even_add_one : even (n + 1) ↔ ¬ even n :=
 by simp [even_add]
 
@@ -127,15 +116,6 @@ by cases mod_two_eq_zero_or_one m with h₁ h₁;
 theorem odd_mul : odd (m * n) ↔ odd m ∧ odd n :=
 by simp [not_or_distrib] with parity_simps
 
-theorem even.mul_left (hm : even m) (n : ℤ) : even (m * n) :=
-even_mul.mpr $ or.inl hm
-
-theorem even.mul_right (m : ℤ) (hn : even n) : even (m * n) :=
-even_mul.mpr $ or.inr hn
-
-theorem odd.mul (hm : odd m) (hn : odd n) : odd (m * n) :=
-odd_mul.mpr ⟨hm, hn⟩
-
 theorem odd.of_mul_left (h : odd (m * n)) : odd m :=
 (odd_mul.mp h).1
 
@@ -160,15 +140,9 @@ lemma ne_of_odd_add (h : odd (m + n)) : m ≠ n :=
 @[parity_simps] theorem odd_sub : odd (m - n) ↔ (odd m ↔ even n) :=
 by rw [odd_iff_not_even, even_sub, not_iff, odd_iff_not_even]
 
-theorem odd.sub_even (hm : odd m) (hn : even n) : odd (m - n) :=
-odd_sub.2 $ iff_of_true hm hn
-
 theorem odd_sub' : odd (m - n) ↔ (odd n ↔ even m) :=
 by rw [odd_iff_not_even, even_sub, not_iff, not_iff_comm, odd_iff_not_even]
 
-theorem even.sub_odd (hm : even m) (hn : odd n) : odd (m - n) :=
-odd_sub'.2 $ iff_of_true hn hm
-
 lemma even_mul_succ_self (n : ℤ) : even (n * (n + 1)) :=
 begin
   rw even_mul,
@@ -198,14 +172,14 @@ begin
     obtain ⟨k, hk⟩ := h,
     convert dvd_mul_right 4 k,
     rw [eq_add_of_sub_eq hk, mul_add, add_assoc, add_sub_cancel, ←mul_assoc],
-    norm_num },
+    refl },
   { left,
     obtain ⟨k, hk⟩ := h,
     convert dvd_mul_right 4 (k + 1),
     rw [eq_sub_of_add_eq hk, add_right_comm, ←add_sub, mul_add, mul_sub, add_assoc, add_assoc,
       sub_add, add_assoc, ←sub_sub (2 * n), sub_self, zero_sub, sub_neg_eq_add, ←mul_assoc,
       mul_add],
-    norm_num },
+    refl },
 end
 
 lemma two_mul_div_two_of_even : even n → 2 * (n / 2) = n := int.mul_div_cancel'

src/data/nat/parity.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Jeremy Avigad, Benjamin Davidson
 -/
 import data.nat.modeq
+import algebra.parity
 
 /-!
 # Parity of natural numbers
@@ -84,14 +85,9 @@ instance decidable_pred_odd : decidable_pred (odd : ℕ → Prop) :=
 
 mk_simp_attribute parity_simps "Simp attribute for lemmas about `even`"
 
-@[simp] theorem even_zero : even 0 := ⟨0, dec_trivial⟩
-
 @[simp] theorem not_even_one : ¬ even 1 :=
 by rw even_iff; norm_num
 
-@[simp] theorem even_bit0 (n : ℕ) : even (bit0 n) :=
-⟨n, by rw [bit0, two_mul]⟩
-
 @[parity_simps] theorem even_add : even (m + n) ↔ (even m ↔ even n) :=
 by cases mod_two_eq_zero_or_one m with h₁ h₁;
    cases mod_two_eq_zero_or_one n with h₂ h₂;
@@ -141,15 +137,6 @@ by cases mod_two_eq_zero_or_one m with h₁ h₁;
 theorem odd_mul : odd (m * n) ↔ odd m ∧ odd n :=
 by simp [not_or_distrib] with parity_simps
 
-theorem even.mul_left (hm : even m) (n) : even (m * n) :=
-even_mul.mpr $ or.inl hm
-
-theorem even.mul_right (m) (hn : even n) : even (m * n) :=
-even_mul.mpr $ or.inr hn
-
-theorem odd.mul (hm : odd m) (hn : odd n) : odd (m * n) :=
-odd_mul.mpr ⟨hm, hn⟩
-
 theorem odd.of_mul_left (h : odd (m * n)) : odd m :=
 (odd_mul.mp h).1
 

src/number_theory/cyclotomic/discriminant.lean

@@ -47,7 +47,7 @@ begin
     rw [← mul_one 2, ← nat.div_mul_div_comm (even_iff_two_dvd.1 h) (one_dvd _), nat.div_one,
       mul_one, mul_comm, pow_mul],
     congr' 1,
-    exact neg_one_pow_of_odd (even.sub_odd (one_le_iff_ne_zero.2 hpos.ne.symm) h (odd_iff.2 rfl)) },
+    exact neg_one_pow_of_odd (nat.even.sub_odd (one_le_iff_ne_zero.2 hpos.ne') h (odd_iff.2 rfl)) },
   { have H := congr_arg derivative (cyclotomic_prime_mul_X_sub_one K p),
     rw [derivative_mul, derivative_sub, derivative_one, derivative_X, sub_zero, mul_one,
       derivative_sub, derivative_one, sub_zero, derivative_X_pow] at H,