Theorems · Theorem · number theory

Polynomial.orderOf_root_cyclotomic_dvd

∀ {n : ℕ} (hpos : 0 < n) {p : ℕ} [inst : Fact (Nat.Prime p)] {a : ℕ}
  (hroot : (Polynomial.cyclotomic n (ZMod p)).IsRoot ((Nat.castRingHom (ZMod p)) a)),
  orderOf (ZMod.unitOfCoprime a ⋯) ∣ n

If (a : ℕ) is a root of cyclotomic n (ZMod p), then the multiplicative order of a modulo p divides n.

Defined in

Mathlib.RingTheory.Polynomial.Cyclotomic.Basic

Cited by

0 results in Mathlib

Foundations

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

Assumes

Fact