# mathlib3documentation

data.mv_polynomial.expand

## 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 n. This operation is called mv_polynomial.expand and it is an algebra homomorphism.

### Main declaration #

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

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

See also polynomial.expand.

Equations
@[simp]
theorem mv_polynomial.expand_C {σ : Type u_1} {R : Type u_3} (p : ) (r : R) :
@[simp]
theorem mv_polynomial.expand_X {σ : Type u_1} {R : Type u_3} (p : ) (i : σ) :
=
@[simp]
theorem mv_polynomial.expand_monomial {σ : Type u_1} {R : Type u_3} (p : ) (d : σ →₀ ) (r : R) :
r) = * d.support.prod (λ (i : σ), ^ p) ^ d i)
theorem mv_polynomial.expand_one_apply {σ : Type u_1} {R : Type u_3} (f : R) :
= f
@[simp]
theorem mv_polynomial.expand_one {σ : Type u_1} {R : Type u_3}  :
= R)
theorem mv_polynomial.expand_comp_bind₁ {σ : Type u_1} {τ : Type u_2} {R : Type u_3} (p : ) (f : σ ) :
= mv_polynomial.bind₁ (λ (i : σ), (f i))
theorem mv_polynomial.expand_bind₁ {σ : Type u_1} {τ : Type u_2} {R : Type u_3} (p : ) (f : σ ) (φ : R) :
( φ) = (mv_polynomial.bind₁ (λ (i : σ), (f i))) φ
@[simp]
theorem mv_polynomial.map_expand {σ : Type u_1} {R : Type u_3} {S : Type u_4} (f : R →+* S) (p : ) (φ : R) :
φ) = ( φ)
@[simp]
theorem mv_polynomial.rename_expand {σ : Type u_1} {τ : Type u_2} {R : Type u_3} (f : σ τ) (p : ) (φ : R) :
φ) = φ)
@[simp]
theorem mv_polynomial.rename_comp_expand {σ : Type u_1} {τ : Type u_2} {R : Type u_3} (f : σ τ) (p : ) :