Theorems · Theorem · number theory

IsCyclotomicExtension.union_left

∀ (S T : Set ℕ) (A : Type u) (B : Type v) [inst : CommRing A] [inst_1 : CommRing B] [inst_2 : Algebra A B]
  [h : IsCyclotomicExtension T A B],
  S ⊆ T → IsCyclotomicExtension S A ↥(Algebra.adjoin A {b | ∃ a ∈ S, a ≠ 0 ∧ b ^ a = 1})

If B is a cyclotomic extension of A given by roots of unity of order in T and S ⊆ T, then adjoin A { b : B | ∃ a : ℕ, a ∈ S ∧ a ≠ 0 ∧ b ^ a = 1 } is a cyclotomic extension of B given by roots of unity of order in S.

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

CommRingCommRingAlgebraIsCyclotomicExtension