Polynomial module #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
Any changes to this file require a corresponding PR to mathlib4.
In this file, we define the polynomial module for an
M, i.e. the
This is defined as an type alias
polynomial_module R M := ℕ →₀ M, since there might be different
module structures on
ℕ →₀ M of interest. See the docstring of
polynomial_module for details.
@[protected, nolint, instance]
This is required to have the
is_scalar_tower S R M instance to avoid diamonds.
m * x ^ i. This is defeq to
finsupp.single_add_hom, and is redefined here
so that it has the desired type signature.
The image of a polynomial under a linear map.
comp p q is the composition of
p : R[X] and
q : M[X] as