chore(data/nat/parity): rename type variable (#6016)

src/data/nat/parity.lean

@@ -9,29 +9,31 @@ import data.nat.modeq
 
 namespace nat
 
-@[simp] theorem mod_two_ne_one {n : ℕ} : ¬ n % 2 = 1 ↔ n % 2 = 0 :=
+variables {m n : ℕ}
+
+@[simp] theorem mod_two_ne_one : ¬ n % 2 = 1 ↔ n % 2 = 0 :=
 by cases mod_two_eq_zero_or_one n with h h; simp [h]
 
-@[simp] theorem mod_two_ne_zero {n : ℕ} : ¬ n % 2 = 0 ↔ n % 2 = 1 :=
+@[simp] theorem mod_two_ne_zero : ¬ n % 2 = 0 ↔ n % 2 = 1 :=
 by cases mod_two_eq_zero_or_one n with h h; simp [h]
 
-theorem even_iff {n : ℕ} : even n ↔ n % 2 = 0 :=
+theorem even_iff : even n ↔ n % 2 = 0 :=
 ⟨λ ⟨m, hm⟩, by simp [hm], λ h, ⟨n / 2, (mod_add_div n 2).symm.trans (by simp [h])⟩⟩
 
-theorem odd_iff {n : ℕ} : odd n ↔ n % 2 = 1 :=
+theorem odd_iff : odd n ↔ n % 2 = 1 :=
 ⟨λ ⟨m, hm⟩, by norm_num [hm, add_mod],
  λ h, ⟨n / 2, (mod_add_div n 2).symm.trans (by rw [h, add_comm])⟩⟩
 
-lemma not_even_iff {n : ℕ} : ¬ even n ↔ n % 2 = 1 :=
+lemma not_even_iff : ¬ even n ↔ n % 2 = 1 :=
 by rw [even_iff, mod_two_ne_zero]
 
-lemma not_odd_iff {n : ℕ} : ¬ odd n ↔ n % 2 = 0 :=
+lemma not_odd_iff : ¬ odd n ↔ n % 2 = 0 :=
 by rw [odd_iff, mod_two_ne_one]
 
-lemma even_iff_not_odd {n : ℕ} : even n ↔ ¬ odd n :=
+lemma even_iff_not_odd : even n ↔ ¬ odd n :=
 by rw [not_odd_iff, even_iff]
 
-@[simp] lemma odd_iff_not_even {n : ℕ} : odd n ↔ ¬ even n :=
+@[simp] lemma odd_iff_not_even : odd n ↔ ¬ even n :=
 by rw [not_even_iff, odd_iff]
 
 lemma even_or_odd (n : ℕ) : even n ∨ odd n :=
@@ -57,7 +59,7 @@ begin
               one_ne_zero, and_self] },
 end
 
-lemma odd_gt_zero {n : ℕ} (h : odd n) : 0 < n :=
+lemma odd_gt_zero (h : odd n) : 0 < n :=
 by { obtain ⟨k, hk⟩ := h, rw hk, exact succ_pos', }
 
 instance : decidable_pred (even : ℕ → Prop) :=
@@ -76,7 +78,7 @@ by rw even_iff; apply one_ne_zero
 @[simp] theorem even_bit0 (n : ℕ) : even (bit0 n) :=
 ⟨n, by rw [bit0, two_mul]⟩
 
-@[parity_simps] theorem even_add {m n : ℕ} : even (m + n) ↔ (even m ↔ even n) :=
+@[parity_simps] theorem even_add : even (m + n) ↔ (even m ↔ even n) :=
 begin
   cases mod_two_eq_zero_or_one m with h₁ h₁; cases mod_two_eq_zero_or_one n with h₂ h₂;
     simp [even_iff, h₁, h₂],
@@ -86,50 +88,47 @@ begin
   exact @modeq.modeq_add _ _ 1 _ 1 h₁ h₂
 end
 
-theorem even.add_even {m n : ℕ} (hm : even m) (hn : even n) : even (m + n) :=
+theorem even.add_even (hm : even m) (hn : even n) : even (m + n) :=
 even_add.2 $ by simp only [*]
 
-theorem even_add' {m n : ℕ} : even (m + n) ↔ (odd m ↔ odd n) :=
+theorem even_add' : even (m + n) ↔ (odd m ↔ odd n) :=
 by rw [even_add, even_iff_not_odd, even_iff_not_odd, not_iff_not]
 
-theorem odd.add_odd {m n : ℕ} (hm : odd m) (hn : odd n) : even (m + n) :=
+theorem odd.add_odd (hm : odd m) (hn : odd n) : even (m + n) :=
 even_add'.2 $ by simp only [*]
 
 @[simp] theorem not_even_bit1 (n : ℕ) : ¬ even (bit1 n) :=
 by simp [bit1] with parity_simps
 
 lemma two_not_dvd_two_mul_add_one (n : ℕ) : ¬(2 ∣ 2 * n + 1) :=
-begin
-  convert not_even_bit1 n,
-  exact two_mul n,
-end
+by convert not_even_bit1 n; exact two_mul n
 
-lemma two_not_dvd_two_mul_sub_one : Π {n : ℕ} (w : 0 < n), ¬(2 ∣ 2 * n - 1) | (n + 1) _ :=
+lemma two_not_dvd_two_mul_sub_one : Π {n} (w : 0 < n), ¬(2 ∣ 2 * n - 1) | (n + 1) _ :=
 two_not_dvd_two_mul_add_one n
 
-@[parity_simps] theorem even_sub {m n : ℕ} (h : n ≤ m) : even (m - n) ↔ (even m ↔ even n) :=
+@[parity_simps] theorem even_sub (h : n ≤ m) : even (m - n) ↔ (even m ↔ even n) :=
 begin
   conv { to_rhs, rw [←nat.sub_add_cancel h, even_add] },
   by_cases h : even n; simp [h]
 end
 
-theorem even.sub_even {m n : ℕ} (hm : even m) (hn : even n) : even (m - n) :=
+theorem even.sub_even (hm : even m) (hn : even n) : even (m - n) :=
 (le_total n m).elim
   (λ h, by simp only [even_sub h, *])
   (λ h, by simp only [sub_eq_zero_of_le h, even_zero])
 
-theorem even_sub' {m n : ℕ} (h : n ≤ m) : even (m - n) ↔ (odd m ↔ odd n) :=
+theorem even_sub' (h : n ≤ m) : even (m - n) ↔ (odd m ↔ odd n) :=
 by rw [even_sub h, even_iff_not_odd, even_iff_not_odd, not_iff_not]
 
-theorem odd.sub_odd {m n : ℕ} (hm : odd m) (hn : odd n) : even (m - n) :=
+theorem odd.sub_odd (hm : odd m) (hn : odd n) : even (m - n) :=
 (le_total n m).elim
   (λ h, by simp only [even_sub' h, *])
   (λ h, by simp only [sub_eq_zero_of_le h, even_zero])
 
-@[parity_simps] theorem even_succ {n : ℕ} : even (succ n) ↔ ¬ even n :=
+@[parity_simps] theorem even_succ : even (succ n) ↔ ¬ even n :=
 by rw [succ_eq_add_one, even_add]; simp [not_even_one]
 
-@[parity_simps] theorem even_mul {m n : ℕ} : even (m * n) ↔ even m ∨ even n :=
+@[parity_simps] theorem even_mul : even (m * n) ↔ even m ∨ even n :=
 begin
   cases mod_two_eq_zero_or_one m with h₁ h₁; cases mod_two_eq_zero_or_one n with h₂ h₂;
     simp [even_iff, h₁, h₂],
@@ -141,61 +140,62 @@ end
 
 /-- If `m` and `n` are natural numbers, then the natural number `m^n` is even
 if and only if `m` is even and `n` is positive. -/
-@[parity_simps] theorem even_pow {m n : ℕ} : even (m^n) ↔ even m ∧ n ≠ 0 :=
+@[parity_simps] theorem even_pow : even (m^n) ↔ even m ∧ n ≠ 0 :=
 by { induction n with n ih; simp [*, pow_succ', even_mul], tauto }
 
-lemma even_div {m n : ℕ} : even (m / n) ↔ m % (2 * n) / n = 0 :=
+lemma even_div  : even (m / n) ↔ m % (2 * n) / n = 0 :=
 by rw [even_iff_two_dvd, dvd_iff_mod_eq_zero, nat.div_mod_eq_mod_mul_div, mul_comm]
 
-@[parity_simps] theorem odd_add {m n : ℕ} : odd (m + n) ↔ (odd m ↔ even n) :=
+@[parity_simps] theorem odd_add : odd (m + n) ↔ (odd m ↔ even n) :=
 begin
   by_contra hnot,
   rw [not_iff, ← even_iff_not_odd, even_add, odd_iff_not_even, ← not_iff] at hnot,
   exact (iff_not_self _).mp hnot,
 end
 
-theorem odd.add_even {m n : ℕ} (hm : odd m) (hn : even n) : odd (m + n) :=
+theorem odd.add_even (hm : odd m) (hn : even n) : odd (m + n) :=
 odd_add.2 $ by simp only [*]
 
-theorem odd_add' {m n : ℕ} : odd (m + n) ↔ (odd n ↔ even m) :=
+theorem odd_add' : odd (m + n) ↔ (odd n ↔ even m) :=
 by rw [add_comm, odd_add]
 
-theorem even.add_odd {m n : ℕ} (hm : even m) (hn : odd n) : odd (m + n) :=
+theorem even.add_odd (hm : even m) (hn : odd n) : odd (m + n) :=
 odd_add'.2 $ by simp only [*]
 
-@[parity_simps] theorem odd_sub {m n : ℕ} (h : n ≤ m) : odd (m - n) ↔ (odd m ↔ even n) :=
+@[parity_simps] theorem odd_sub (h : n ≤ m) : odd (m - n) ↔ (odd m ↔ even n) :=
 begin
   by_contra hnot,
   rw [not_iff, ← even_iff_not_odd, even_sub h, odd_iff_not_even, ← not_iff] at hnot,
   exact (iff_not_self _).mp hnot,
 end
 
-theorem odd.sub_even {m n : ℕ} (h : n ≤ m) (hm : odd m) (hn : even n) : odd (m - n) :=
+theorem odd.sub_even (h : n ≤ m) (hm : odd m) (hn : even n) : odd (m - n) :=
 (odd_sub h).mpr (iff_of_true hm hn)
 
-theorem odd_sub' {m n : ℕ} (h : n ≤ m) : odd (m - n) ↔ (odd n ↔ even m) :=
+theorem odd_sub' (h : n ≤ m) : odd (m - n) ↔ (odd n ↔ even m) :=
 begin
   by_contra hnot,
   rw [not_iff, ← even_iff_not_odd, even_sub h, odd_iff_not_even, ← not_iff,
       @iff.comm _ (even n)] at hnot,
   exact (iff_not_self _).mp hnot,
 end
 
-theorem even.sub_odd {m n : ℕ} (h : n ≤ m) (hm : even m) (hn : odd n) : odd (m - n) :=
+theorem even.sub_odd (h : n ≤ m) (hm : even m) (hn : odd n) : odd (m - n) :=
 (odd_sub' h).mpr (iff_of_true hn hm)
 
-theorem neg_one_pow_eq_one_iff_even {α : Type*} [ring α] {n : ℕ} (h1 : (-1 : α) ≠ 1) :
-  (-1 : α) ^ n = 1 ↔ even n :=
+variables {R : Type*} [ring R]
+
+theorem neg_one_pow_eq_one_iff_even (h1 : (-1 : R) ≠ 1) : (-1 : R) ^ n = 1 ↔ even n :=
 ⟨λ h, n.mod_two_eq_zero_or_one.elim (dvd_iff_mod_eq_zero _ _).2
   (λ hn, by rw [neg_one_pow_eq_pow_mod_two, hn, pow_one] at h; exact (h1 h).elim),
   λ ⟨m, hm⟩, by rw [neg_one_pow_eq_pow_mod_two, hm]; simp⟩
 
-@[simp] theorem neg_one_pow_two {α : Type*} [ring α] : (-1 : α) ^ 2 = 1 := by simp
+@[simp] theorem neg_one_pow_two : (-1 : R) ^ 2 = 1 := by simp
 
-theorem neg_one_pow_of_even {α : Type*} [ring α] {n : ℕ} : even n → (-1 : α) ^ n = 1 :=
+theorem neg_one_pow_of_even : even n → (-1 : R) ^ n = 1 :=
 by { rintro ⟨c, rfl⟩, simp [pow_mul] }
 
-theorem neg_one_pow_of_odd {α : Type*} [ring α] {n : ℕ} : odd n → (-1 : α) ^ n = -1 :=
+theorem neg_one_pow_of_odd : odd n → (-1 : R) ^ n = -1 :=
 by { rintro ⟨c, rfl⟩, simp [pow_add, pow_mul] }
 
 -- Here are examples of how `parity_simps` can be used with `nat`.