isGalois_of_isSplittingField_X_pow_sub_C

English

If L/K is the splitting field of X^n − C a with a irreducible and there exist primitive nth roots of unity in K, then L/K is Galois.

Русский

Если L/K является разворачивающим полем X^n − C a с ирредуцируемым a и в K существуют корни единства n-го порядка, то L/K Галуа.

LaTeX

$$$\text{IsGalois}(K,L).$$$

Lean4

theorem isGalois_of_isSplittingField_X_pow_sub_C : IsGalois K L :=
  IsGalois.of_separable_splitting_field (separable_X_pow_sub_C_of_irreducible hζ a H)

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