isSeparable_adjoin_simple_iff_isSeparable

English

Algebra.IsSeparable F F⟮x⟯ iff IsSeparable F x.

Русский

Алгебраическая сепарабельность F⟮x⟯ над F эквивалентна IsSeparable F x.

LaTeX

$$$ Algebra.IsSeparable F F⟮x⟯ \iff IsSeparable F x $$$

Lean4

/-- `F⟮x⟯ / F` is a separable extension if and only if `x` is a separable element.
As a consequence, any rational function of `x` is also a separable element. -/
theorem isSeparable_adjoin_simple_iff_isSeparable {x : E} : Algebra.IsSeparable F F⟮x⟯ ↔ IsSeparable F x :=
  by
  refine ⟨fun _ ↦ ?_, fun hsep ↦ ?_⟩
  · exact isSeparable_of_mem_isSeparable F E <| mem_adjoin_simple_self F x
  · have h := IsSeparable.isIntegral hsep
    haveI := adjoin.finiteDimensional h
    rwa [← finSepDegree_eq_finrank_iff, finSepDegree_adjoin_simple_eq_finrank_iff F E x h.isAlgebraic]

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