Theorems · Theorem · number theory

IsPrimitiveRoot.sum_eq_zero_iff_forall_eq

∀ {K : Type u_1} [inst : Field K] [CharZero K] {p : ℕ} {ζ : K},
  Nat.Prime p → IsPrimitiveRoot ζ p → ∀ (α : Fin p → ℚ), ∑ i, ↑(α i) * ζ ^ ↑i = 0 ↔ ∀ (i j : Fin p), α i = α j

For a prime p, a ℚ-linear combination ∑_{i < p} αᵢ ζⁱ vanishes if and only if all coefficients αᵢ are equal. This follows from the irreducibility of the p-th cyclotomic polynomial. See de Launey–Flannery, Algebraic Design Theory, Lemma 2.8.5.

Defined in

Mathlib.RingTheory.Polynomial.Cyclotomic.Roots

Cited by

1 results in Mathlib

Foundations

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

Assumes

FieldCharZero