Separating elements in transcendence degree one

A finitely generated extension of a perfect field admits a finite separating transcendence basis. When the extension has transcendence degree one, that basis consists of one element. Thus there is a transcendental x such that the extension is separable algebraic over the simple field k(x).

This is the one-variable form of Mathlib's exists_isTranscendenceBasis_and_isSeparable_of_perfectField. It is useful for passing from abstract separable generation to constructions that require a single separating parameter.

Reference

H. Stichtenoth, Algebraic Function Fields and Codes, second edition, Proposition 3.10.2.

theorem TauCeti.exists_transcendental_and_isSeparable_adjoin_of_perfectField {k : Type u} {F : Type v} [Field k] [Field F] [Algebra k F] [PerfectField k] [Algebra.EssFiniteType k F] (htr : Algebra.trdeg k F = 1) : ∃ (x : F), Transcendental k x ∧ Algebra.IsSeparable (↥k⟮x⟯) F

A finitely generated extension of transcendence degree one over a perfect field has a separating element: an element x transcendental over the base such that the extension is separable algebraic over k(x).

This is the singleton form of exists_isTranscendenceBasis_and_isSeparable_of_perfectField.