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
.
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
The power basis 1, x, ..., x ^ (d - 1)
for K[x]
,
where d
is the degree of the minimal polynomial of x
. See algebra.adjoin.power_basis'
for
a version over a more general base ring.
Equations
- algebra.adjoin.power_basis hx = {gen := ⟨x, _⟩, dim := (minpoly K x).nat_degree, basis := algebra.adjoin.power_basis_aux hx, basis_eq_pow := _}
The power basis given by x
if B.gen ∈ adjoin K {x}
. See power_basis.of_gen_mem_adjoin'
for a version over a more general base ring.
Equations
- B.of_gen_mem_adjoin hint hx = (algebra.adjoin.power_basis hint).map (((algebra.adjoin K {x}).equiv_of_eq ⊤ _).trans subalgebra.top_equiv)
If B : power_basis S A
is such that is_integral R B.gen
, then
is_integral R (B.basis.repr (B.gen ^ n) i)
for all i
if
minpoly S B.gen = (minpoly R B.gen).map (algebra_map R S)
. This is the case if R
is a GCD domain
and S
is its fraction ring.
Let B : power_basis S A
be such that is_integral R B.gen
, and let x y : A
be elements with
integral coordinates in the base B.basis
. Then is_integral R ((B.basis.repr (x * y) i)
for all
i
if minpoly S B.gen = (minpoly R B.gen).map (algebra_map R S)
. This is the case if R
is a GCD
domain and S
is its fraction ring.
Let B : power_basis S A
be such that is_integral R B.gen
, and let x : A
be and element
with integral coordinates in the base B.basis
. Then is_integral R ((B.basis.repr (x ^ n) i)
for
all i
and all n
if minpoly S B.gen = (minpoly R B.gen).map (algebra_map R S)
. This is the case
if R
is a GCD domain and S
is its fraction ring.
Let B B' : power_basis K S
be such that is_integral R B.gen
, and let P : R[X]
be such that
aeval B.gen P = B'.gen
. Then is_integral R (B.basis.to_matrix B'.basis i j)
for all i
and j
if minpoly K B.gen = (minpoly R B.gen).map (algebra_map R L)
. This is the case
if R
is a GCD domain and K
is its fraction ring.