English
The triple A, CyclotomicRing n A K, CyclotomicField n K forms a scalar tower: actions are compatible across the chain A → CyclotomicRing → CyclotomicField.
Русский
Тройка A, CyclotomicRing n A K, CyclotomicField n K образует кубик-цепь скаляров: действие скаляров совместимо на всем пути A → CyclotomicRing → CyclotomicField.
LaTeX
$$$\\text{IsScalarTower} A\\; (\\operatorname{CyclotomicRing}(n,A,K))\\; (\\operatorname{CyclotomicField}(n,K))$$$
Lean4
/-- Separably closed fields are `S`-cyclotomic extensions over themselves if
`NeZero ((a : ℕ) : K)` for all nonzero `a ∈ S`. -/
theorem isCyclotomicExtension (h : ∀ a ∈ S, a ≠ 0 → NeZero (a : K)) : IsCyclotomicExtension S K K :=
by
refine ⟨fun {a} ha ha' ↦ ?_, Algebra.eq_top_iff.mp <| Subsingleton.elim _ _⟩
have := h a ha ha'
obtain ⟨r, hr⟩ :=
IsSepClosed.exists_aeval_eq_zero K _ (degree_cyclotomic_pos a K (Nat.pos_of_ne_zero ha')).ne'
(separable_cyclotomic a K)
exact ⟨r, by rwa [coe_aeval_eq_eval, ← IsRoot.def, isRoot_cyclotomic_iff] at hr⟩
