powerBasisAux — Mathlib

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)

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