mathlib documentation

ring_theory.adjoin.power_basis

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) :
is_basis K (λ (i : fin (minpoly K x).nat_degree), x, _⟩ ^ i)
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) :

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

Equations