English
If x is integral over K, then the K-vector space adjoin_K({x}) possesses a basis consisting of the powers 1, x, x^2, ..., x^{d-1}, where d is the degree of the minimal polynomial of x over K.
Русский
Если x интеграл над полем K, то пространство над K, порождаемое x, имеет базис из степеней x: 1, x, x^2, ..., x^{d-1}, где d — степень минимального многочлена x над K.
LaTeX
$$$\text{If } hx: \text{IsIntegral } K x, \text{ then } \text{powerBasisAux}_{K,S}(x,hx) \text{ is a basis with } d = \operatorname{natDegree}(\minpoly K x).$$$
Lean4
/-- The elements `1, x, ..., x ^ (d - 1)` for a basis for the `K`-module `K[x]`,
where `d` is the degree of the minimal polynomial of `x`. -/
noncomputable def powerBasisAux {x : S} (hx : IsIntegral K x) :
Basis (Fin (minpoly K x).natDegree) K (adjoin K ({ x } : Set S)) :=
by
have hST : Function.Injective (algebraMap (adjoin K ({ x } : Set S)) S) := Subtype.coe_injective
have hx' : IsIntegral K (⟨x, subset_adjoin (Set.mem_singleton x)⟩ : adjoin K ({ x } : Set S)) :=
by
apply (isIntegral_algebraMap_iff hST).mp
convert hx
apply Basis.mk (v := fun i : Fin _ ↦ ⟨x, subset_adjoin (Set.mem_singleton x)⟩ ^ (i : ℕ))
· have : LinearIndependent K _ := linearIndependent_pow (⟨x, self_mem_adjoin_singleton _ _⟩ : adjoin K { x })
rwa [← minpoly.algebraMap_eq hST] at this
· rintro ⟨y, hy⟩ _
have := hx'.mem_span_pow (y := ⟨y, hy⟩)
rw [← minpoly.algebraMap_eq hST] at this
apply this
rw [adjoin_singleton_eq_range_aeval] at hy
obtain ⟨f, rfl⟩ := (aeval x).mem_range.mp hy
use f
ext
exact aeval_algebraMap_apply S (⟨x, _⟩ : adjoin K { x }) _
