English
If ζ ∈ L is a primitive n-th root of unity, then IsCyclotomicExtension {n} K (IntermediateField.adjoin K {ζ}).
Русский
Пусть ζ ∈ L является примитивным корнем единицы степени n. Тогда IsCyclotomicExtension {n} K (IntermediateField.adjoin K {ζ}).
LaTeX
$$$[IsPrimitiveRoot\\, ζ\\, n] \\Rightarrow IsCyclotomicExtension\\{n\\} K (\\text{IntermediateField.adjoin } K\\{ζ\\})$$$
Lean4
/-- A cyclotomic extension is integral. -/
theorem integral [IsCyclotomicExtension S A B] : Algebra.IsIntegral A B :=
by
rw [←
(Subalgebra.equivOfEq _ _ ((IsCyclotomicExtension.iff_adjoin_eq_top S A B).1 ‹_›).2 |>.trans
Subalgebra.topEquiv).isIntegral_iff]
exact Algebra.IsIntegral.adjoin fun x ⟨n, hn, h1, h2⟩ ↦ ⟨X ^ n - 1, monic_X_pow_sub_C 1 h1, by simp [h2]⟩
