# Documentation

Mathlib.Data.MvPolynomial.Expand

## Expand multivariate polynomials #

Given a multivariate polynomial φ, one may replace every occurrence of X i by X i ^ n, for some natural number n. This operation is called MvPolynomial.expand and it is an algebra homomorphism.

### Main declaration #

• MvPolynomial.expand: expand a polynomial by a factor of p, so ∑ aₙ xⁿ becomes ∑ aₙ xⁿᵖ.
noncomputable def MvPolynomial.expand {σ : Type u_1} {R : Type u_3} [] (p : ) :

Expand the polynomial by a factor of p, so ∑ aₙ xⁿ becomes ∑ aₙ xⁿᵖ.

Instances For
theorem MvPolynomial.expand_C {σ : Type u_1} {R : Type u_3} [] (p : ) (r : R) :
↑() (MvPolynomial.C r) = MvPolynomial.C r
@[simp]
theorem MvPolynomial.expand_X {σ : Type u_1} {R : Type u_3} [] (p : ) (i : σ) :
↑() () =
@[simp]
theorem MvPolynomial.expand_monomial {σ : Type u_1} {R : Type u_3} [] (p : ) (d : σ →₀ ) (r : R) :
↑() (↑() r) = MvPolynomial.C r * Finset.prod d.support fun i => () ^ d i
theorem MvPolynomial.expand_one_apply {σ : Type u_1} {R : Type u_3} [] (f : ) :
↑() f = f
@[simp]
theorem MvPolynomial.expand_one {σ : Type u_1} {R : Type u_3} [] :
= AlgHom.id R ()
theorem MvPolynomial.expand_comp_bind₁ {σ : Type u_1} {τ : Type u_2} {R : Type u_3} [] (p : ) (f : σ) :
= MvPolynomial.bind₁ fun i => ↑() (f i)
theorem MvPolynomial.expand_bind₁ {σ : Type u_1} {τ : Type u_2} {R : Type u_3} [] (p : ) (f : σ) (φ : ) :
↑() (↑() φ) = ↑(MvPolynomial.bind₁ fun i => ↑() (f i)) φ
@[simp]
theorem MvPolynomial.map_expand {σ : Type u_1} {R : Type u_3} {S : Type u_4} [] [] (f : R →+* S) (p : ) (φ : ) :
↑() (↑() φ) = ↑() (↑() φ)
@[simp]
theorem MvPolynomial.rename_expand {σ : Type u_1} {τ : Type u_2} {R : Type u_3} [] (f : στ) (p : ) (φ : ) :
↑() (↑() φ) = ↑() (↑() φ)
@[simp]
theorem MvPolynomial.rename_comp_expand {σ : Type u_1} {τ : Type u_2} {R : Type u_3} [] (f : στ) (p : ) :