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} [CommSemiring R] (p : ℕ) : MvPolynomial σ R →ₐ[R] MvPolynomial σ R

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

See also Polynomial.expand.

Equations

• MvPolynomial.expand p = { toRingHom := MvPolynomial.eval₂Hom MvPolynomial.C fun (i : σ) => MvPolynomial.X i ^ p, commutes' := ⋯ }

theorem MvPolynomial.expand_C {σ : Type u_1} {R : Type u_3} [CommSemiring R] (p : ℕ) (r : R) : (MvPolynomial.expand p) (MvPolynomial.C r) = MvPolynomial.C r

@[simp]

theorem MvPolynomial.expand_X {σ : Type u_1} {R : Type u_3} [CommSemiring R] (p : ℕ) (i : σ) : (MvPolynomial.expand p) (MvPolynomial.X i) = MvPolynomial.X i ^ p

@[simp]

theorem MvPolynomial.expand_monomial {σ : Type u_1} {R : Type u_3} [CommSemiring R] (p : ℕ) (d : σ →₀ ℕ) (r : R) : (MvPolynomial.expand p) ((MvPolynomial.monomial d) r) = MvPolynomial.C r * ∏ i ∈ d.support, (MvPolynomial.X i ^ p) ^ d i

theorem MvPolynomial.expand_one_apply {σ : Type u_1} {R : Type u_3} [CommSemiring R] (f : MvPolynomial σ R) : (MvPolynomial.expand 1) f = f

@[simp]

theorem MvPolynomial.expand_one {σ : Type u_1} {R : Type u_3} [CommSemiring R] : MvPolynomial.expand 1 = AlgHom.id R (MvPolynomial σ R)

theorem MvPolynomial.expand_comp_bind₁ {σ : Type u_1} {τ : Type u_2} {R : Type u_3} [CommSemiring R] (p : ℕ) (f : σ → MvPolynomial τ R) : (MvPolynomial.expand p).comp (MvPolynomial.bind₁ f) = MvPolynomial.bind₁ fun (i : σ) => (MvPolynomial.expand p) (f i)

theorem MvPolynomial.expand_bind₁ {σ : Type u_1} {τ : Type u_2} {R : Type u_3} [CommSemiring R] (p : ℕ) (f : σ → MvPolynomial τ R) (φ : MvPolynomial σ R) : (MvPolynomial.expand p) ((MvPolynomial.bind₁ f) φ) = (MvPolynomial.bind₁ fun (i : σ) => (MvPolynomial.expand p) (f i)) φ

@[simp]

theorem MvPolynomial.map_expand {σ : Type u_1} {R : Type u_3} {S : Type u_4} [CommSemiring R] [CommSemiring S] (f : R →+* S) (p : ℕ) (φ : MvPolynomial σ R) : (MvPolynomial.map f) ((MvPolynomial.expand p) φ) = (MvPolynomial.expand p) ((MvPolynomial.map f) φ)

@[simp]

theorem MvPolynomial.rename_expand {σ : Type u_1} {τ : Type u_2} {R : Type u_3} [CommSemiring R] (f : σ → τ) (p : ℕ) (φ : MvPolynomial σ R) : (MvPolynomial.rename f) ((MvPolynomial.expand p) φ) = (MvPolynomial.expand p) ((MvPolynomial.rename f) φ)

@[simp]

theorem MvPolynomial.rename_comp_expand {σ : Type u_1} {τ : Type u_2} {R : Type u_3} [CommSemiring R] (f : σ → τ) (p : ℕ) : (MvPolynomial.rename f).comp (MvPolynomial.expand p) = (MvPolynomial.expand p).comp (MvPolynomial.rename f)