Theorems · Theorem · number theory

IsCyclotomicExtension.adjoin_roots

∀ {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] (x : B), x ∈ Algebra.adjoin A {b | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1}

The n-th roots of unity, for n ∈ S nonzero, generate B as an A-algebra.

Defined in

Mathlib.NumberTheory.Cyclotomic.Basic

Cited by

2 results in Mathlib

Foundations

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

Assumes

IsCyclotomicExtension