add_dvd_pow_add_pow — Mathlib

English

For odd n and any ring R, x + y divides x^n + y^n when x, y ∈ R and R is commutative.

Русский

При нечетном n и в коммутативном кольце R сумма x + y делит x^n + y^n.

LaTeX

$$$\\displaystyle x + y \\;|\\; x^n + y^n$ (для нечетного n)$$

Lean4

theorem add_dvd_pow_add_pow (x y : R) {n : ℕ} (h : Odd n) : x + y ∣ x ^ n + y ^ n :=
  by
  have h₁ := geom_sum₂_mul x (-y) n
  rw [Odd.neg_pow h y, sub_neg_eq_add, sub_neg_eq_add] at h₁
  exact Dvd.intro_left _ h₁

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