English
Let L/K be an S-cyclotomic extension. Then L is a separable extension of K.
Русский
Пусть K ⊆ L и L/K является S-циклотомическим расширением. Тогда расширение L/K раздельно.
LaTeX
$$$IsCyclotomicExtension(S,K,L) \\Rightarrow Separable(K,L)$$$
Lean4
theorem isSeparable [IsCyclotomicExtension S K L] : Algebra.IsSeparable K L :=
by
have := integral S K L
have h := (IsCyclotomicExtension.iff_adjoin_eq_top S K L).1 ‹_› |>.2
rw [← IntermediateField.adjoin_algebraic_toSubalgebra fun b _ ↦ Algebra.IsAlgebraic.isAlgebraic b, ←
IntermediateField.top_toSubalgebra] at h
rw [←
AlgEquiv.Algebra.isSeparable_iff <|
(IntermediateField.equivOfEq (IntermediateField.toSubalgebra_injective h)).trans IntermediateField.topEquiv,
IntermediateField.isSeparable_adjoin_iff_isSeparable]
rintro b ⟨n, hn, h1, h2⟩
have := NeZero.mk h1
have := Polynomial.X_pow_sub_one_separable_iff.2 (neZero_of_mem' n S K L hn).out
exact this.of_dvd <| minpoly.dvd K b <| by simp [h2]
