Coefficient vectors under variable embeddings #
The embedding Polynomial.toMvPolynomial i reindexes the native coefficient vector
by sending an exponent n to the multivariate exponent Finsupp.single i n.
This description lets coefficient constructions commute with placement in one coordinate.
In particular, the partial degree of the placed polynomial in Xᵢ is its degree.
theorem
Polynomial.coeff_toMvPolynomial_eq_embDomain
{R : Type u_1}
{σ : Type u_2}
[CommSemiring R]
(p : Polynomial R)
(i : σ)
:
((toMvPolynomial i) p).coeff = Finsupp.embDomain { toFun := Finsupp.single i, inj' := ⋯ } p.toFinsupp.coeff
Placement in one coordinate reindexes the native coefficient vector by the corresponding single-coordinate exponent embedding.
@[simp]
theorem
Polynomial.degreeOf_toMvPolynomial
{R : Type u_1}
{σ : Type u_2}
[CommSemiring R]
(p : Polynomial R)
(i : σ)
:
Placement in the coordinate Xᵢ turns the degree into the partial degree in Xᵢ.