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.
noncomputable
def
algebra.adjoin.power_basis_aux
{K : Type u_1}
{S : Type u_2}
[field K]
[comm_ring S]
[algebra K S]
{x : S}
(hx : is_integral K x) :
basis (fin (minpoly K x).nat_degree) K ↥(algebra.adjoin 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
@[simp]
theorem
algebra.adjoin.power_basis_gen
{K : Type u_1}
{S : Type u_2}
[field K]
[comm_ring S]
[algebra K S]
{x : S}
(hx : is_integral K x) :
(algebra.adjoin.power_basis hx).gen = ⟨x, _⟩
@[simp]
theorem
algebra.adjoin.power_basis_dim
{K : Type u_1}
{S : Type u_2}
[field K]
[comm_ring S]
[algebra K S]
{x : S}
(hx : is_integral K x) :
(algebra.adjoin.power_basis hx).dim = (minpoly K x).nat_degree
noncomputable
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, basis := algebra.adjoin.power_basis_aux hx, basis_eq_pow := _}