Theorems · Theorem · number theory

IsCyclotomicExtension.exists_isPrimitiveRoot

∀ {S : Set ℕ} (A : Type u) (B : Type v) {inst : CommRing A} {inst_1 : CommRing B} {inst_2 : Algebra A B}
  [self : IsCyclotomicExtension S A B] {n : ℕ}, n ∈ S → n ≠ 0 → ∃ r, IsPrimitiveRoot r n

For all nonzero n ∈ S, there exists a primitive n-th root of unity in B.

Defined in

Mathlib.NumberTheory.Cyclotomic.Basic

Cited by

14 results in Mathlib

Foundations

Depth 7 from the axioms · uses no axioms

Assumes

IsCyclotomicExtension