theorem pow_sub_pow_eq_prod_sub_zeta_runity_mul {K : Type u_1} [CommRing K] [IsDomain K] {ζ : K} {n : ℕ} (hpos : 0 < n) (h : IsPrimitiveRoot ζ n) (x : K) (y : K) : x ^ n - y ^ n = Finset.prod (Polynomial.nthRootsFinset n K) fun ζ => x - ζ * y

If there is a primitive nth root of unity in K, then X ^ n - Y ^ n = ∏ (X - μ Y), where μ varies over the n-th roots of unity.

theorem pow_add_pow_eq_prod_add_zeta_runity_mul {K : Type u_1} [CommRing K] [IsDomain K] {ζ : K} {n : ℕ} (hodd : n % 2 = 1) (h : IsPrimitiveRoot ζ n) (x : K) (y : K) : x ^ n + y ^ n = Finset.prod (Polynomial.nthRootsFinset n K) fun ζ => x + ζ * y

If there is a primitive nth root of unity in K and n is odd, then X ^ n + Y ^ n = ∏ (X + μ Y), where μ varies over the n-th roots of unity.