English
For integral x over K, there is a natural power-basis of the K-algebra adjoin_K({x}) given by powers of x up to d-1, where d is the degree of the minimal polynomial of x over K.
Русский
Пусть x интеграл над K. Тогда над K существует естественный базис степени для алгебры adjoin_K({x}) из степеней x: 1, x, ..., x^{d-1}, где d — степень минимального многочлена x над K.
LaTeX
$$$\text{powerBasis } {x} : \text{PowerBasis } K (\mathrm{adjoin}_K(\{x\}))$$$
Lean4
/-- The power basis `1, x, ..., x ^ (d - 1)` for `K[x]`,
where `d` is the degree of the minimal polynomial of `x`. See `Algebra.adjoin.powerBasis'` for
a version over a more general base ring. -/
@[simps gen dim]
noncomputable def powerBasis {x : S} (hx : IsIntegral K x) : PowerBasis K (adjoin K ({ x } : Set S))
where
gen := ⟨x, subset_adjoin (Set.mem_singleton x)⟩
dim := (minpoly K x).natDegree
basis := adjoin.powerBasisAux hx
basis_eq_pow i := by rw [adjoin.powerBasisAux, Basis.mk_apply]
