Theorems · Theorem · number theory

IsCyclotomicExtension.union_of_isPrimitiveRoot

∀ {n : ℕ} [NeZero n] (S : Set ℕ) (A : Type u) (B : Type v) [inst : CommRing A] [inst_1 : CommRing B]
  [inst_2 : Algebra A B] [hB : IsCyclotomicExtension S A B] {r : B},
  IsPrimitiveRoot r n → IsCyclotomicExtension (S ∪ {n}) A B

If there exists a primitive root of unity of order n in B, then IsCyclotomicExtension S A B implies IsCyclotomicExtension (S ∪ {n}) A B.

Defined in

Mathlib.NumberTheory.Cyclotomic.Basic

Cited by

1 results in Mathlib

Foundations

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

Assumes

NeZeroCommRingCommRingAlgebraIsCyclotomicExtension