Theorems · Theorem · number theory

IsPrimitiveRoot.pow_sub_pow_eq_prod_sub_mul

∀ {R : Type u_1} [inst : CommRing R] {ζ : R} {n : ℕ} (x y : R) [inst_1 : IsDomain R],
  0 < n → IsPrimitiveRoot ζ n → x ^ n - y ^ n = ∏ ζ ∈ Polynomial.nthRootsFinset n 1, (x - ζ * y)

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

Defined in

Mathlib.RingTheory.Polynomial.Cyclotomic.Basic

Cited by

1 results in Mathlib

Foundations

Depth 141 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommRingIsDomain