Theory of univariate polynomials #
The main defs here are
We give several lemmas about their interaction with each other and with module operations.
Evaluate a polynomial
p given a ring hom
f from the scalar ring
to the target and a value
x for the variable in the target
eval₂ as a
ring_hom for noncommutative rings
We next prove that eval₂ is multiplicative as long as target ring is commutative (even if the source ring is not).
After having set up the basic theory of
Perhaps we can make the others irreducible too?