Theorems · Theorem · number theory

IsPrimitiveRoot.squarefree_minpoly_mod

∀ {n : ℕ} {K : Type u_1} [inst : CommRing K] {μ : K},
  IsPrimitiveRoot μ n →
    ∀ [IsDomain K] [CharZero K] {p : ℕ} [inst_3 : Fact (Nat.Prime p)],
      ¬p ∣ n → Squarefree (Polynomial.map (Int.castRingHom (ZMod p)) (minpoly ℤ μ))

The reduction modulo p of the minimal polynomial of a root of unity μ is squarefree.

Defined in

Mathlib.RingTheory.RootsOfUnity.Minpoly

Cited by

1 results in Mathlib

Foundations

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

Assumes

CommRingIsDomainCharZeroFact