# 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.

def algebra.adjoin.power_basis_aux {K : Type u_1} {S : Type u_2} [field K] [comm_ring S] [ S] {x : S} (hx : x) :
basis (fin (minpoly K x).nat_degree) K {x})

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.

Equations
def algebra.adjoin.power_basis {K : Type u_1} {S : Type u_2} [field K] [comm_ring S] [ S] {x : S} (hx : x) :
{x})

The power basis 1, x, ..., x ^ (d - 1) for K[x], where d is the degree of the minimal polynomial of x.

Equations