card_aut_eq_finrank — Mathlib

English

Let E be finite over F with an element α ∈ E integral over F and separable over F, and suppose the minimal polynomial of α splits over F(α). Then the number of F-automorphisms of F(α) equals the degree [F(α):F].

Русский

Пусть E/F конечно, α ∈ E целочислен над F и сепарерав над F, и минимальный полином α распадается в F(α). Тогда число F‑автоморфизмов F(α) равно степени расширения [F(α):F].

LaTeX

$$Nat.card (F⟮α⟯ ≃ₐ[F] F⟮α⟯) = finrank F F⟮α⟯$$

Lean4

theorem card_aut_eq_finrank [FiniteDimensional F E] {α : E} (hα : IsIntegral F α) (h_sep : IsSeparable F α)
    (h_splits : (minpoly F α).Splits (algebraMap F F⟮α⟯)) : Nat.card (F⟮α⟯ ≃ₐ[F] F⟮α⟯) = finrank F F⟮α⟯ :=
  by
  rw [IntermediateField.adjoin.finrank hα]
  rw [← IntermediateField.card_algHom_adjoin_integral F hα h_sep h_splits]
  exact Nat.card_congr (algEquivEquivAlgHom F F⟮α⟯)

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