adjoin_eq_top_of_primitive_element

English

Gal(K/k) is viewed as a profinite group by taking the automorphism group Aut_k(K) and forming the associated ProfiniteGrp.

Русский

Галуа(K/k) рассматривается как профинитная группа через группу автоморфизмов Aut_k(K) и соответствующую ProfiniteGrp.

LaTeX

$$profiniteGalGrp k K = ProfiniteGrp.of (K ≃ₐ[k] K)$$

Lean4

theorem _root_.Algebra.adjoin_eq_top_of_primitive_element {α : E} (hα : IsIntegral F α) (hα₂ : F⟮α⟯ = ⊤) :
    Algebra.adjoin F { α } = ⊤ :=
  Algebra.adjoin_eq_top_of_intermediateField (by simpa [isAlgebraic_iff_isIntegral]) hα₂

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