card_algHom_adjoin_integral — Mathlib

English

The cardinality of the set of algebra homomorphisms from the adjoint field to K equals the degree of the minimal polynomial, under suitable separability and splitting conditions.

Русский

Число морфизмов от сопряженного поля к K равно степени минимального полинома при подходящих условиях разделимости и разбиения.

LaTeX

$$Nat.card (F⟮α⟯ →ₐ[F] K) = (minpoly F α).natDegree$$

Lean4

theorem card_algHom_adjoin_integral (h : IsIntegral F α) (h_sep : IsSeparable F α)
    (h_splits : (minpoly F α).Splits (algebraMap F K)) : Nat.card (F⟮α⟯ →ₐ[F] K) = (minpoly F α).natDegree :=
  by
  let _ : Fintype (F⟮α⟯ →ₐ[F] K) := fintypeOfAlgHomAdjoinIntegral F h
  rw [Nat.card_eq_fintype_card, AlgHom.card_of_powerBasis] <;>
    simp only [IsSeparable, adjoin.powerBasis_dim, adjoin.powerBasis_gen, minpoly_gen, h_splits]
  exact h_sep

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