splitting_field_cyclotomic — Mathlib

English

If L/K is {n}-cyclotomic, then L is the splitting field of X^n - 1 over K.

Русский

Если L/K циклотомическое по {n}, то L — разворачивающее поле для многочлена X^n - 1 над K.

LaTeX

$$$IsCyclotomicExtension\\{n\\} K L \\Rightarrow IsSplittingField(K,L,X^n-1)$$$

Lean4

/-- If `IsCyclotomicExtension {n} K L`, then `L` is the splitting field of `cyclotomic n K`. -/
theorem splitting_field_cyclotomic : IsSplittingField K L (cyclotomic n K) :=
  { splits' := splits_cyclotomic K L (mem_singleton n)
    adjoin_rootSet' := by
      rw [← ((iff_adjoin_eq_top { n } K L).1 inferInstance).2]
      letI := Classical.decEq L
      obtain ⟨ζ : L, hζ⟩ := IsCyclotomicExtension.exists_isPrimitiveRoot K L (mem_singleton n) (NeZero.ne _)
      exact adjoin_roots_cyclotomic_eq_adjoin_nth_roots hζ }

Похожие утверждения