Theory of univariate polynomials #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
Any changes to this file require a corresponding PR to mathlib4.
The theorems include formulas for computing coefficients, such as
The nth coefficient, as a linear map.
constant_coeff p returns the constant term of the polynomial
coeff p 0. This is a ring homomorphism.