primitive_element_iff_algHom_eq_of_eval'

English

The finite intermediate field theorem provides a definition of a finite-dimensional field using the concept of a primitive element and a power basis.

Русский

Теорема о конечном промежуточном поле задает существование конечномерного базиса через примитивный элемент и степенной базис.

LaTeX

$$defined as:PowerBasis$$

Lean4

theorem primitive_element_iff_algHom_eq_of_eval' (α : E) : F⟮α⟯ = ⊤ ↔ Function.Injective fun φ : E →ₐ[F] A ↦ φ α := by
  classical
    simp_rw [primitive_element_iff_minpoly_natDegree_eq, ←
    card_rootSet_eq_natDegree (K := A) (Algebra.IsSeparable.isSeparable F α) (hA _), ← toFinset_card, ←
    (Algebra.IsAlgebraic.of_finite F E).range_eval_eq_rootSet_minpoly_of_splits _ hA α, ←
    AlgHom.card_of_splits F E A hA, Fintype.card, toFinset_range, Finset.card_image_iff, Finset.coe_univ, ←
    injective_iff_injOn_univ]

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