Theorems · Theorem · number theory

IsPrimitiveRoot.minpoly_dvd_mod_p

∀ {n : ℕ} {K : Type u_1} [inst : CommRing K] {μ : K},
  IsPrimitiveRoot μ n →
    ∀ [IsDomain K] [CharZero K] {p : ℕ} [inst_3 : Fact (Nat.Prime p)],
      ¬p ∣ n →
        Polynomial.map (Int.castRingHom (ZMod p)) (minpoly ℤ μ) ∣
          Polynomial.map (Int.castRingHom (ZMod 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 prime that does not divide n. Then P divides Q modulo p.

Defined in

Mathlib.RingTheory.RootsOfUnity.Minpoly

Cited by

1 results in Mathlib

Foundations

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

Assumes

CommRingIsDomainCharZeroFact