Theorems · Theorem · number theory

IsCyclotomicExtension.adjoin_primitive_root_eq_top

∀ {A : Type u} {B : Type v} [inst : CommRing A] [inst_1 : CommRing B] [inst_2 : Algebra A B] {n : ℕ} [NeZero n]
  [IsDomain B] [h : IsCyclotomicExtension {n} A B] {ζ : B}, IsPrimitiveRoot ζ n → A[ζ] = ⊤

Defined in

Mathlib.NumberTheory.Cyclotomic.Basic

Cited by

0 results in Mathlib

Foundations

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

Assumes

CommRingCommRingAlgebraNeZeroIsDomainIsCyclotomicExtension