Power basis for algebra.adjoin R {x} #
This file defines the canonical power basis on algebra.adjoin R {x},
where x is an integral element over R.
theorem
algebra.power_basis_is_basis
{K : Type u_1}
{S : Type u_2}
[field K]
[comm_ring S]
[algebra K S]
{x : S}
(hx : is_integral K x) :
def
algebra.adjoin.power_basis
{K : Type u_1}
{S : Type u_2}
[field K]
[comm_ring S]
[algebra K S]
{x : S}
(hx : is_integral K x) :
power_basis K ↥(algebra.adjoin K {x})
The power basis 1, x, ..., x ^ (d - 1) for K[x],
where d is the degree of the minimal polynomial of x.
Equations
- algebra.adjoin.power_basis hx = {gen := ⟨x, _⟩, dim := (minpoly K x).nat_degree, is_basis := _}