Expand multivariate polynomials #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
Any changes to this file require a corresponding PR to mathlib4.
Given a multivariate polynomial
φ, one may replace every occurence of
X i by
X i ^ n,
for some natural number
This operation is called
mv_polynomial.expand and it is an algebra homomorphism.
Main declaration #
Expand the polynomial by a factor of p, so
∑ aₙ xⁿ becomes
∑ aₙ xⁿᵖ.