Theory of univariate polynomials #
We show that
polynomial A is an R-algebra when
A is an R-algebra.
eval₂ to an algebra hom in
Note that this instance also provides
algebra R R[X].
When we have
[comm_semiring R], the function
C is the same as
algebra_map R R[X].
(But note that
C is defined when
R is not necessarily commutative, in which case
algebra_map is not available.)
Extensionality lemma for algebra maps out of
polynomial A' over a smaller base ring than
Algebra isomorphism between
polynomial R and
add_monoid_algebra R ℕ. This is just an
implementation detail, but it can be useful to transfer results from
finsupp to polynomials.
Given a valuation
x of the variable in an
aeval R A x is
R-algebra homomorphism from
This is a stronger variant of the linear map
aeval for defining algebra homs out of
polynomial R over a smaller base ring
The evaluation map is not generally multiplicative when the coefficient ring is noncommutative,
but nevertheless any polynomial of the form
p * (X - monomial 0 r) is sent to zero
when evaluated at
This is the key step in our proof of the Cayley-Hamilton theorem.