Theory of univariate polynomials #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
Any changes to this file require a corresponding PR to mathlib4.
We show that
A[X] 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
A'[X] over a smaller base ring than
Algebra isomorphism between
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
R[X] 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.