instIsGaloisOfFinite — Mathlib

English

If K ⊆ K' with K' finite, then the extension K/K' is Galois.

Русский

Если имеется конечное поле K', то расширение K ⊆ K' является Галуа-расширением.

LaTeX

$$IsGalois K K'$$

Lean4

instance (priority := 100) {K K' : Type*} [Field K] [Field K'] [Finite K'] [Algebra K K'] : IsGalois K K' :=
  by
  cases nonempty_fintype K'
  obtain ⟨p, hp⟩ := CharP.exists K
  haveI : CharP K p := hp
  haveI : CharP K' p := charP_of_injective_algebraMap' K K' p
  exact
    IsGalois.of_separable_splitting_field
      (galois_poly_separable p (Fintype.card K')
        (let ⟨n, _, hn⟩ := FiniteField.card K' p
        hn.symm ▸ dvd_pow_self p n.ne_zero))

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