simp only [mul_neg, sub_neg_eq_add] at this
K : Type u_1
inst✝¹ : CommRing K
inst✝ : IsDomain K
ζ : K
n : ℕ
hodd : n % 2 = 1
h : IsPrimitiveRoot ζ n
x y : K
this : x ^ n - (-y) ^ n = ∏ ζ ∈ nthRootsFinset n K, (x - ζ * -y)
⊢ x ^ n + y ^ n = ∏ ζ ∈ nthRootsFinset n K, (x + ζ * y)
K : Type u_1
inst✝¹ : CommRing K
inst✝ : IsDomain K
ζ : K
n : ℕ
hodd : n % 2 = 1
h : IsPrimitiveRoot ζ n
x y : K
this : x ^ n - (-y) ^ n = ∏ x_1 ∈ nthRootsFinset n K, (x + x_1 * y)
⊢ x ^ n + y ^ n = ∏ ζ ∈ nthRootsFinset n K, (x + ζ * y)