English
If S ⊆ T, then the adjoin of A by roots of unity corresponding to S yields a cyclotomic extension of A over S inside B.
Русский
Если S ⊆ T, то адъянт A по корням единицы, соответствующим S, образует циклотомическое расширение A над S внутри B.
LaTeX
$$If hS: S ⊆ T, then IsCyclotomicExtension S A (adjoin A {b : B | ∃ a ∈ S, a ≠ 0 ∧ b^a = 1}) B$$
Lean4
/-- 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`. -/
theorem union_left [h : IsCyclotomicExtension T A B] (hS : S ⊆ T) :
IsCyclotomicExtension S A (adjoin A {b : B | ∃ a : ℕ, a ∈ S ∧ a ≠ 0 ∧ b ^ a = 1}) :=
by
refine ⟨fun {n} hn hn' => ?_, fun b => ?_⟩
· obtain ⟨b, hb⟩ := ((isCyclotomicExtension_iff _ _ _).1 h).1 (hS hn) hn'
refine ⟨⟨b, subset_adjoin ⟨n, hn, hn', hb.pow_eq_one⟩⟩, ?_⟩
rwa [← IsPrimitiveRoot.coe_submonoidClass_iff, Subtype.coe_mk]
· convert mem_top (R := A) (x := b)
rw [← adjoin_adjoin_coe_preimage, preimage_setOf_eq]
norm_cast
