Theorems · Theorem · number theory

IsPrimitiveRoot.minpoly_eq_pow

∀ {n : ℕ} {K : Type u_1} [inst : CommRing K] {μ : K},
  IsPrimitiveRoot μ n →
    ∀ [IsDomain K] [CharZero K] {p : ℕ} [hprime : Fact (Nat.Prime p)], ¬p ∣ n → minpoly ℤ μ = minpoly ℤ (μ ^ p)

If p is a prime that does not divide n, then the minimal polynomials of a primitive n-th root of unity μ and of μ ^ p are the same.

Defined in

Mathlib.RingTheory.RootsOfUnity.Minpoly

Cited by

1 results in Mathlib

Foundations

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

Assumes

CommRingIsDomainCharZeroFact