Theorems · Theorem · number theory

IsPrimitiveRoot.dvd_of_isCyclotomicExtension

∀ (n : ℕ) [NeZero n] {K : Type u} [inst : Field K] [inst_1 : NumberField K] [IsCyclotomicExtension {n} ℚ K] {ζ : K}
  {l : ℕ}, IsPrimitiveRoot ζ l → l ≠ 0 → l ∣ 2 * n

If an n-th cyclotomic extension of ℚ contains a primitive l-th root of unity, then l ∣ 2 * n.

Defined in

Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots

Cited by

1 results in Mathlib

Foundations

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

Assumes

NeZeroFieldNumberFieldIsCyclotomicExtension