eight_dvd_sq_sub_one_of_odd — Mathlib

English

For p prime and Odd p, and x,y ∈ ℕ with p ∣ x − y and p ∤ x, for any odd n, emultiplicity p (x^n − y^n) = emultiplicity p (x − y) + emultiplicity p n.

Русский

Для p простого и нечетного, и x,y ∈ ℕ с p | x−y и p ∤ x, при нечетном n выполняется LTE: v_p(x^n − y^n) = v_p(x − y) + v_p(n).

LaTeX

$$∀ p ∈ ℕ, Prime p, Odd p, ∀ x,y ∈ ℕ, if p ∣ (x − y) ∧ p ∤ x, ∀ n ∈ ℕ, Odd n → emultiplicity p (x^n − y^n) = emultiplicity p (x − y) + emultiplicity p n.$$

Lean4

theorem eight_dvd_sq_sub_one_of_odd {k : ℕ} (hk : Odd k) : 8 ∣ k ^ 2 - 1 :=
  by
  rcases hk with ⟨m, rfl⟩
  have eq : (2 * m + 1) ^ 2 - 1 = 4 * (m * (m + 1)) := by ring_nf; grind
  simpa [eq] using (mul_dvd_mul_iff_left four_ne_zero).mpr (two_dvd_mul_add_one m)

Похожие утверждения