finSepDegree_adjoin_simple_le_finrank

English

If α is algebraic over F, then the separable degree of F⟮α⟯/F equals the natSepDegree of its minimal polynomial.

Русский

Если α над F алгебраичен, то разделительная степень расширения F⟮α⟯/F равна natSepDegree его минимального многочлена.

LaTeX

$$$ finSepDegree F F⟮α⟯ = (minpoly F α).natSepDegree $$$

Lean4

/-- The separable degree of `F⟮α⟯ / F` is smaller than the degree of `F⟮α⟯ / F` if `α` is
algebraic over `F`. -/
theorem finSepDegree_adjoin_simple_le_finrank (α : E) (halg : IsAlgebraic F α) : finSepDegree F F⟮α⟯ ≤ finrank F F⟮α⟯ :=
  by
  haveI := adjoin.finiteDimensional halg.isIntegral
  exact Nat.le_of_dvd finrank_pos <| finSepDegree_adjoin_simple_dvd_finrank F E α

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