Power basis #
This file defines a structure
power_basis R S, giving a basis of the
S as a finite list of powers
1, x, ..., x^n.
For example, if
x is algebraic over a ring/field, adjoining
power_basis structure generated by
power_basis R A: a structure containing an
1, x, ..., x^nis a basis for the
A(viewed as an
power_basis.equiv: if two power bases satisfy the same equations, they are equivalent as algebras
Implementation notes #
power basis, powerbasis
- gen : S
- dim : ℕ
- basis : basis (fin c.dim) R S
- basis_eq_pow : ∀ (i : fin c.dim), ⇑(c.basis) i = c.gen ^ ↑i
pb : power_basis R S states that
1, pb.gen, ..., pb.gen ^ (pb.dim - 1)
is a basis for the
S (viewed as
This is a structure, not a class, since the same algebra can have many power bases.
For the common case where
S is defined by adjoining an integral element to
the canonical power basis is given by
pb.minpoly_gen is a minimal polynomial for
A is not a field, it might not necessarily be the minimal polynomial,
nat_degree_minpoly shows its degree is indeed minimal.
pb.lift y hy is the algebra map sending
hy states the higher powers of
y are the same as the higher powers of
pb.equiv pb' h is an equivalence of algebras with the same power basis.
Useful lemma to show
x generates a power basis:
the powers of
x less than the degree of
x's minimal polynomial are linearly independent.