Theorems · Theorem · number theory

IsPrimitiveRoot.exists_neg_pow_of_isOfFinOrder

∀ {n : ℕ} [NeZero n] {K : Type u} [inst : Field K] [inst_1 : NumberField K] [IsCyclotomicExtension {n} ℚ K],
  Odd n → ∀ {ζ x : K}, IsPrimitiveRoot ζ n → IsOfFinOrder x → ∃ r, x = (-ζ) ^ r

If x is a root of unity (spelled as IsOfFinOrder x) in an n-th cyclotomic extension of ℚ, where n is odd, and ζ is a primitive n-th root of unity, then there exist r such that x = (-ζ)^r.

Defined in

Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots

Cited by

1 results in Mathlib

Foundations

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

Assumes

NeZeroFieldNumberFieldIsCyclotomicExtension