Theorems · Theorem · number theory

Polynomial.coprime_of_root_cyclotomic

∀ {n : ℕ},
  0 < n →
    ∀ {p : ℕ} [hprime : Fact (Nat.Prime p)] {a : ℕ},
      (Polynomial.cyclotomic n (ZMod p)).IsRoot ((Nat.castRingHom (ZMod p)) a) → a.Coprime p

If (a : ℕ) is a root of cyclotomic n (ZMod p), where p is a prime, then a and p are coprime.

Defined in

Mathlib.RingTheory.Polynomial.Cyclotomic.Basic

Cited by

2 results in Mathlib

Foundations

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

Assumes

Fact