English
An instance showing {0}-cyclotomic extension: IsCyclotomicExtension {0} K (CyclotomicField 0 K).
Русский
Пример: IsCyclotomicExtension {0} K (CyclotomicField 0 K).
LaTeX
$$$IsCyclotomicExtension\\{0\\} K (CyclotomicField 0 K)$$$
Lean4
instance isCyclotomicExtension [NeZero (n : K)] : IsCyclotomicExtension { n } K (CyclotomicField n K) :=
by
have : NeZero (n : CyclotomicField n K) := NeZero.nat_of_injective (algebraMap K _).injective
letI := Classical.decEq (CyclotomicField n K)
obtain ⟨ζ, hζ⟩ :=
exists_root_of_splits (algebraMap K (CyclotomicField n K)) (SplittingField.splits _)
(degree_cyclotomic_pos n K (NeZero.pos n)).ne'
rw [← eval_map, ← IsRoot.def, map_cyclotomic, isRoot_cyclotomic_iff] at hζ
refine ⟨?_, ?_⟩
· simp only [mem_singleton_iff, forall_eq]
exact fun _ ↦ ⟨ζ, hζ⟩
· rw [← Algebra.eq_top_iff, ← SplittingField.adjoin_rootSet, eq_comm]
exact IsCyclotomicExtension.adjoin_roots_cyclotomic_eq_adjoin_nth_roots hζ
