finSepDegree_adjoin_simple_eq_finrank_iff

English

Let α ∈ E be algebraic over F. Then finSepDegree F F⟮α⟯ = finrank F F⟮α⟯ if and only if α is separable over F.

Русский

Пусть α ∈ E алгебраически над F. Тогда finSepDegree F F⟮α⟯ = finrank F F⟮α⟯ тогда и только тогда α-разделимо над F.

LaTeX

$$$ finSepDegree F F⟮α⟯ = finrank F F⟮α⟯ \iff IsSeparable F α $$$

Lean4

/-- If `α` is algebraic over `F`, then the separable degree of `F⟮α⟯ / F` is equal to the degree
of `F⟮α⟯ / F` if and only if `α` is a separable element. -/
theorem finSepDegree_adjoin_simple_eq_finrank_iff (α : E) (halg : IsAlgebraic F α) :
    finSepDegree F F⟮α⟯ = finrank F F⟮α⟯ ↔ IsSeparable F α := by
  rw [finSepDegree_adjoin_simple_eq_natSepDegree F E halg, adjoin.finrank halg.isIntegral,
    natSepDegree_eq_natDegree_iff _ (minpoly.ne_zero halg.isIntegral), IsSeparable]

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