Theorems · Theorem · number theory

IsPrimitiveRoot.minpoly_dvd_expand

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

Let P be the minimal polynomial of a root of unity μ and Q be the minimal polynomial of μ ^ p, where p is a natural number that does not divide n. Then P divides expand ℤ p Q.

Defined in

Mathlib.RingTheory.RootsOfUnity.Minpoly

Cited by

1 results in Mathlib

Foundations

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

Assumes

CommRingIsDomainCharZero