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}
[comm_semiring R]
(p : ℕ) :
mv_polynomial σ R →ₐ[R] mv_polynomial σ R
Expand the polynomial by a factor of p, so ∑ aₙ xⁿ becomes ∑ aₙ xⁿᵖ.
See also polynomial.expand.
Equations
- mv_polynomial.expand p = {to_fun := (mv_polynomial.eval₂_hom mv_polynomial.C (λ (i : σ), mv_polynomial.X i ^ p)).to_fun, map_one' := _, map_mul' := _, map_zero' := _, map_add' := _, commutes' := _}
@[simp]
@[simp]
theorem
mv_polynomial.expand_X
{σ : Type u_1}
{R : Type u_3}
[comm_semiring R]
(p : ℕ)
(i : σ) :
⇑(mv_polynomial.expand p) (mv_polynomial.X i) = mv_polynomial.X i ^ p
@[simp]
theorem
mv_polynomial.expand_monomial
{σ : Type u_1}
{R : Type u_3}
[comm_semiring R]
(p : ℕ)
(d : σ →₀ ℕ)
(r : R) :
⇑(mv_polynomial.expand p) (⇑(mv_polynomial.monomial d) r) = ⇑mv_polynomial.C r * d.support.prod (λ (i : σ), (mv_polynomial.X i ^ p) ^ ⇑d i)
theorem
mv_polynomial.expand_one_apply
{σ : Type u_1}
{R : Type u_3}
[comm_semiring R]
(f : mv_polynomial σ R) :
⇑(mv_polynomial.expand 1) f = f
@[simp]
theorem
mv_polynomial.expand_one
{σ : Type u_1}
{R : Type u_3}
[comm_semiring R] :
mv_polynomial.expand 1 = alg_hom.id R (mv_polynomial σ R)
theorem
mv_polynomial.expand_comp_bind₁
{σ : Type u_1}
{τ : Type u_2}
{R : Type u_3}
[comm_semiring R]
(p : ℕ)
(f : σ → mv_polynomial τ R) :
(mv_polynomial.expand p).comp (mv_polynomial.bind₁ f) = mv_polynomial.bind₁ (λ (i : σ), ⇑(mv_polynomial.expand p) (f i))
theorem
mv_polynomial.expand_bind₁
{σ : Type u_1}
{τ : Type u_2}
{R : Type u_3}
[comm_semiring R]
(p : ℕ)
(f : σ → mv_polynomial τ R)
(φ : mv_polynomial σ R) :
⇑(mv_polynomial.expand p) (⇑(mv_polynomial.bind₁ f) φ) = ⇑(mv_polynomial.bind₁ (λ (i : σ), ⇑(mv_polynomial.expand p) (f i))) φ
@[simp]
theorem
mv_polynomial.map_expand
{σ : Type u_1}
{R : Type u_3}
{S : Type u_4}
[comm_semiring R]
[comm_semiring S]
(f : R →+* S)
(p : ℕ)
(φ : mv_polynomial σ R) :
⇑(mv_polynomial.map f) (⇑(mv_polynomial.expand p) φ) = ⇑(mv_polynomial.expand p) (⇑(mv_polynomial.map f) φ)
@[simp]
theorem
mv_polynomial.rename_expand
{σ : Type u_1}
{τ : Type u_2}
{R : Type u_3}
[comm_semiring R]
(f : σ → τ)
(p : ℕ)
(φ : mv_polynomial σ R) :
⇑(mv_polynomial.rename f) (⇑(mv_polynomial.expand p) φ) = ⇑(mv_polynomial.expand p) (⇑(mv_polynomial.rename f) φ)
@[simp]
theorem
mv_polynomial.rename_comp_expand
{σ : Type u_1}
{τ : Type u_2}
{R : Type u_3}
[comm_semiring R]
(f : σ → τ)
(p : ℕ) :