α : Type u
inst✝ : CommRing α
x y : α
n : ℕ
h : Odd n
h₁ : (∑ i in range n, x ^ i * (-y) ^ (n - 1 - i)) * (x - -y) = x ^ n - (-y) ^ n
⊢ x + y ∣ x ^ n + y ^ n
α : Type u
inst✝ : CommRing α
x y : α
n : ℕ
h : Odd n
⊢ x + y ∣ x ^ n + y ^ n
have h₁ := geom_sum₂_mul x (-y) n
α : Type u
inst✝ : CommRing α
x y : α
n : ℕ
h : Odd n
h₁ : (∑ i in range n, x ^ i * (-y) ^ (n - 1 - i)) * (x + y) = x ^ n + y ^ n
⊢ x + y ∣ x ^ n + y ^ n
α : Type u
inst✝ : CommRing α
x y : α
n : ℕ
h : Odd n
h₁ : (∑ i in range n, x ^ i * (-y) ^ (n - 1 - i)) * (x - -y) = x ^ n - (-y) ^ n
⊢ x + y ∣ x ^ n + y ^ n
rw [Odd.neg_pow h y, sub_neg_eq_add, sub_neg_eq_add] at h₁
no goals
α : Type u
inst✝ : CommRing α
x y : α
n : ℕ
h : Odd n
h₁ : (∑ i in range n, x ^ i * (-y) ^ (n - 1 - i)) * (x + y) = x ^ n + y ^ n
⊢ x + y ∣ x ^ n + y ^ n
exact Dvd.intro_left _ h₁