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 := _}