English
If x is integral over K, then K⟮x⟯ is an algebraic extension of K.
Русский
Если x интегрально над полем K, то K⟮x⟯ — алгебраическое расширение K.
LaTeX
$$If \IsIntegral K x then Algebra.IsAlgebraic K K⟮x⟯$$
Lean4
/-- The elements `1, x, ..., x ^ (d - 1)` form a basis for `K⟮x⟯`,
where `d` is the degree of the minimal polynomial of `x`. -/
noncomputable def powerBasisAux {x : L} (hx : IsIntegral K x) : Basis (Fin (minpoly K x).natDegree) K K⟮x⟯ :=
(AdjoinRoot.powerBasis (minpoly.ne_zero hx)).basis |>.map (adjoinRootEquivAdjoin K hx).toLinearEquiv |>.reindex
(finCongr rfl)