feat: Int.{even_sub_one,even_mul_pred_self} (#9859)

Also rename `Nat.even_mul_self_pred` for consistency with `Nat.even_mul_succ_self`.
leanprover-community · Jan 26, 2024 · 0500719 · 0500719
1 parent 970a1ab
commit 0500719
Show file tree

Hide file tree

Showing 4 changed files with 14 additions and 9 deletions.
diff --git a/Mathlib/Algebra/GroupPower/NegOnePow.lean b/Mathlib/Algebra/GroupPower/NegOnePow.lean
@@ -88,11 +88,6 @@ lemma negOnePow_eq_iff (n₁ n₂ : ℤ) :
 
 @[simp]
 lemma negOnePow_mul_self (n : ℤ) : (n * n).negOnePow = n.negOnePow := by
-  suffices Even (n * (n - 1)) by
-    simpa [mul_sub, mul_one, negOnePow_eq_iff] using this
-  rw [even_mul]
-  by_cases h : Even (n - 1)
-  · exact Or.inr h
-  · exact Or.inl (by simpa using Int.even_add_one.2 h)
+  simpa [mul_sub, negOnePow_eq_iff] using n.even_mul_pred_self
 
 end Int
diff --git a/Mathlib/Data/Int/Parity.lean b/Mathlib/Data/Int/Parity.lean
@@ -135,6 +135,10 @@ theorem even_add_one : Even (n + 1) ↔ ¬Even n := by
   simp [even_add]
 #align int.even_add_one Int.even_add_one
 
+@[parity_simps]
+theorem even_sub_one : Even (n - 1) ↔ ¬Even n := by
+  simp [even_sub]
+
 @[parity_simps]
 theorem even_mul : Even (m * n) ↔ Even m ∨ Even n := by
   cases' emod_two_eq_zero_or_one m with h₁ h₁ <;>
@@ -196,6 +200,9 @@ theorem even_mul_succ_self (n : ℤ) : Even (n * (n + 1)) := by
   simpa [even_mul, parity_simps] using n.even_or_odd
 #align int.even_mul_succ_self Int.even_mul_succ_self
 
+theorem even_mul_pred_self (n : ℤ) : Even (n * (n - 1)) := by
+  simpa [even_mul, parity_simps] using n.even_or_odd
+
 @[simp, norm_cast]
 theorem even_coe_nat (n : ℕ) : Even (n : ℤ) ↔ Even n := by
   rw_mod_cast [even_iff, Nat.even_iff]

diff --git a/Mathlib/Data/Nat/Parity.lean b/Mathlib/Data/Nat/Parity.lean
@@ -217,10 +217,13 @@ theorem even_mul_succ_self (n : ℕ) : Even (n * (n + 1)) := by
   exact em _
 #align nat.even_mul_succ_self Nat.even_mul_succ_self
 
-theorem even_mul_self_pred : ∀ n : ℕ, Even (n * (n - 1))
+theorem even_mul_pred_self : ∀ n : ℕ, Even (n * (n - 1))
   | 0 => even_zero
   | (n + 1) => mul_comm (n + 1 - 1) (n + 1) ▸ even_mul_succ_self n
-#align nat.even_mul_self_pred Nat.even_mul_self_pred
+#align nat.even_mul_self_pred Nat.even_mul_pred_self
+
+@[deprecated] -- 2024-01-20
+alias even_mul_self_pred := even_mul_pred_self
 
 theorem two_mul_div_two_of_even : Even n → 2 * (n / 2) = n := fun h =>
   Nat.mul_div_cancel_left' (even_iff_two_dvd.mp h)

diff --git a/Mathlib/RingTheory/Discriminant.lean b/Mathlib/RingTheory/Discriminant.lean
@@ -215,7 +215,7 @@ theorem discr_powerBasis_eq_prod'' [IsSeparable K L] (e : Fin pb.dim ≃ (L →
   have hn : n = pb.dim := by
     rw [← AlgHom.card K L E, ← Fintype.card_fin pb.dim]
     exact card_congr (Equiv.symm e)
-  have h₂ : 2 ∣ pb.dim * (pb.dim - 1) := even_iff_two_dvd.1 (Nat.even_mul_self_pred _)
+  have h₂ : 2 ∣ pb.dim * (pb.dim - 1) := pb.dim.even_mul_pred_self.two_dvd
   have hne : ((2 : ℕ) : ℚ) ≠ 0 := by simp
   have hle : 1 ≤ pb.dim := by
     rw [← hn, Nat.one_le_iff_ne_zero, ← zero_lt_iff, FiniteDimensional.finrank_pos_iff]