Documentation

Mathlib.RingTheory.MvPowerSeries.Basic

Formal (multivariate) power series #

This file defines multivariate formal power series and develops the basic properties of these objects.

A formal power series is to a polynomial like an infinite sum is to a finite sum.

We provide the natural inclusion from multivariate polynomials to multivariate formal power series.

Main definitions #

Note #

This file sets up the (semi)ring structure on multivariate power series: additional results are in:

In Mathlib.RingTheory.PowerSeries.Basic, formal power series in one variable will be obtained as a particular case, defined by PowerSeries R := MvPowerSeries Unit R. See that file for a specific description.

Implementation notes #

In this file we define multivariate formal power series with variables indexed by σ and coefficients in R as MvPowerSeries σ R := (σ →₀ ℕ) → R. Unfortunately there is not yet enough API to show that they are the completion of the ring of multivariate polynomials. However, we provide most of the infrastructure that is needed to do this. Once I-adic completion (topological or algebraic) is available it should not be hard to fill in the details.

def MvPowerSeries (σ : Type u_1) (R : Type u_2) :
Type (max (max u_2 0) u_1)

Multivariate formal power series, where σ is the index set of the variables and R is the coefficient ring.

Equations
Instances For
    instance MvPowerSeries.instInhabited {σ : Type u_1} {R : Type u_2} [Inhabited R] :
    Equations
    • MvPowerSeries.instInhabited = { default := fun (x : σ →₀ ) => default }
    instance MvPowerSeries.instZero {σ : Type u_1} {R : Type u_2} [Zero R] :
    Equations
    • MvPowerSeries.instZero = Pi.instZero
    instance MvPowerSeries.instAddMonoid {σ : Type u_1} {R : Type u_2} [AddMonoid R] :
    Equations
    • MvPowerSeries.instAddMonoid = Pi.addMonoid
    instance MvPowerSeries.instAddGroup {σ : Type u_1} {R : Type u_2} [AddGroup R] :
    Equations
    • MvPowerSeries.instAddGroup = Pi.addGroup
    Equations
    • MvPowerSeries.instAddCommMonoid = Pi.addCommMonoid
    Equations
    • MvPowerSeries.instAddCommGroup = Pi.addCommGroup
    instance MvPowerSeries.instNontrivial {σ : Type u_1} {R : Type u_2} [Nontrivial R] :
    Equations
    • =
    instance MvPowerSeries.instModule {σ : Type u_1} {R : Type u_2} {A : Type u_3} [Semiring R] [AddCommMonoid A] [Module R A] :
    Equations
    instance MvPowerSeries.instIsScalarTower {σ : Type u_1} {R : Type u_2} {A : Type u_3} {S : Type u_4} [Semiring R] [Semiring S] [AddCommMonoid A] [Module R A] [Module S A] [SMul R S] [IsScalarTower R S A] :
    Equations
    • =
    def MvPowerSeries.monomial {σ : Type u_1} (R : Type u_2) [Semiring R] (n : σ →₀ ) :

    The nth monomial as multivariate formal power series: it is defined as the R-linear map from R to the semi-ring of multivariate formal power series associating to each a the map sending n : σ →₀ ℕ to the value a and sending all other x : σ →₀ ℕ different from n to 0.

    Equations
    Instances For
      def MvPowerSeries.coeff {σ : Type u_1} (R : Type u_2) [Semiring R] (n : σ →₀ ) :

      The nth coefficient of a multivariate formal power series.

      Equations
      Instances For
        theorem MvPowerSeries.ext_iff {σ : Type u_1} {R : Type u_2} [Semiring R] {φ : MvPowerSeries σ R} {ψ : MvPowerSeries σ R} :
        φ = ψ ∀ (n : σ →₀ ), (MvPowerSeries.coeff R n) φ = (MvPowerSeries.coeff R n) ψ

        Two multivariate formal power series are equal if and only if all their coefficients are equal.

        theorem MvPowerSeries.ext {σ : Type u_1} {R : Type u_2} [Semiring R] {φ : MvPowerSeries σ R} {ψ : MvPowerSeries σ R} (h : ∀ (n : σ →₀ ), (MvPowerSeries.coeff R n) φ = (MvPowerSeries.coeff R n) ψ) :
        φ = ψ

        Two multivariate formal power series are equal if all their coefficients are equal.

        theorem MvPowerSeries.monomial_def {σ : Type u_1} {R : Type u_2} [Semiring R] [DecidableEq σ] (n : σ →₀ ) :
        MvPowerSeries.monomial R n = LinearMap.single R (fun (x : σ →₀ ) => R) n
        theorem MvPowerSeries.coeff_monomial {σ : Type u_1} {R : Type u_2} [Semiring R] [DecidableEq σ] (m : σ →₀ ) (n : σ →₀ ) (a : R) :
        (MvPowerSeries.coeff R m) ((MvPowerSeries.monomial R n) a) = if m = n then a else 0
        @[simp]
        theorem MvPowerSeries.coeff_monomial_same {σ : Type u_1} {R : Type u_2} [Semiring R] (n : σ →₀ ) (a : R) :
        theorem MvPowerSeries.coeff_monomial_ne {σ : Type u_1} {R : Type u_2} [Semiring R] {m : σ →₀ } {n : σ →₀ } (h : m n) (a : R) :
        theorem MvPowerSeries.eq_of_coeff_monomial_ne_zero {σ : Type u_1} {R : Type u_2} [Semiring R] {m : σ →₀ } {n : σ →₀ } {a : R} (h : (MvPowerSeries.coeff R m) ((MvPowerSeries.monomial R n) a) 0) :
        m = n
        @[simp]
        theorem MvPowerSeries.coeff_comp_monomial {σ : Type u_1} {R : Type u_2} [Semiring R] (n : σ →₀ ) :
        MvPowerSeries.coeff R n ∘ₗ MvPowerSeries.monomial R n = LinearMap.id
        @[simp]
        theorem MvPowerSeries.coeff_zero {σ : Type u_1} {R : Type u_2} [Semiring R] (n : σ →₀ ) :
        instance MvPowerSeries.instOne {σ : Type u_1} {R : Type u_2} [Semiring R] :
        Equations
        theorem MvPowerSeries.coeff_one {σ : Type u_1} {R : Type u_2} [Semiring R] (n : σ →₀ ) [DecidableEq σ] :
        (MvPowerSeries.coeff R n) 1 = if n = 0 then 1 else 0
        theorem MvPowerSeries.coeff_zero_one {σ : Type u_1} {R : Type u_2} [Semiring R] :
        Equations
        instance MvPowerSeries.instMul {σ : Type u_1} {R : Type u_2} [Semiring R] :
        Equations
        theorem MvPowerSeries.coeff_mul {σ : Type u_1} {R : Type u_2} [Semiring R] (n : σ →₀ ) (φ : MvPowerSeries σ R) (ψ : MvPowerSeries σ R) [DecidableEq σ] :
        (MvPowerSeries.coeff R n) (φ * ψ) = pFinset.antidiagonal n, (MvPowerSeries.coeff R p.1) φ * (MvPowerSeries.coeff R p.2) ψ
        theorem MvPowerSeries.zero_mul {σ : Type u_1} {R : Type u_2} [Semiring R] (φ : MvPowerSeries σ R) :
        0 * φ = 0
        theorem MvPowerSeries.mul_zero {σ : Type u_1} {R : Type u_2} [Semiring R] (φ : MvPowerSeries σ R) :
        φ * 0 = 0
        theorem MvPowerSeries.coeff_monomial_mul {σ : Type u_1} {R : Type u_2} [Semiring R] (m : σ →₀ ) (n : σ →₀ ) (φ : MvPowerSeries σ R) (a : R) :
        (MvPowerSeries.coeff R m) ((MvPowerSeries.monomial R n) a * φ) = if n m then a * (MvPowerSeries.coeff R (m - n)) φ else 0
        theorem MvPowerSeries.coeff_mul_monomial {σ : Type u_1} {R : Type u_2} [Semiring R] (m : σ →₀ ) (n : σ →₀ ) (φ : MvPowerSeries σ R) (a : R) :
        (MvPowerSeries.coeff R m) (φ * (MvPowerSeries.monomial R n) a) = if n m then (MvPowerSeries.coeff R (m - n)) φ * a else 0
        theorem MvPowerSeries.coeff_add_monomial_mul {σ : Type u_1} {R : Type u_2} [Semiring R] (m : σ →₀ ) (n : σ →₀ ) (φ : MvPowerSeries σ R) (a : R) :
        theorem MvPowerSeries.coeff_add_mul_monomial {σ : Type u_1} {R : Type u_2} [Semiring R] (m : σ →₀ ) (n : σ →₀ ) (φ : MvPowerSeries σ R) (a : R) :
        @[simp]
        theorem MvPowerSeries.commute_monomial {σ : Type u_1} {R : Type u_2} [Semiring R] (φ : MvPowerSeries σ R) {a : R} {n : σ →₀ } :
        Commute φ ((MvPowerSeries.monomial R n) a) ∀ (m : σ →₀ ), Commute ((MvPowerSeries.coeff R m) φ) a
        theorem MvPowerSeries.one_mul {σ : Type u_1} {R : Type u_2} [Semiring R] (φ : MvPowerSeries σ R) :
        1 * φ = φ
        theorem MvPowerSeries.mul_one {σ : Type u_1} {R : Type u_2} [Semiring R] (φ : MvPowerSeries σ R) :
        φ * 1 = φ
        theorem MvPowerSeries.mul_add {σ : Type u_1} {R : Type u_2} [Semiring R] (φ₁ : MvPowerSeries σ R) (φ₂ : MvPowerSeries σ R) (φ₃ : MvPowerSeries σ R) :
        φ₁ * (φ₂ + φ₃) = φ₁ * φ₂ + φ₁ * φ₃
        theorem MvPowerSeries.add_mul {σ : Type u_1} {R : Type u_2} [Semiring R] (φ₁ : MvPowerSeries σ R) (φ₂ : MvPowerSeries σ R) (φ₃ : MvPowerSeries σ R) :
        (φ₁ + φ₂) * φ₃ = φ₁ * φ₃ + φ₂ * φ₃
        theorem MvPowerSeries.mul_assoc {σ : Type u_1} {R : Type u_2} [Semiring R] (φ₁ : MvPowerSeries σ R) (φ₂ : MvPowerSeries σ R) (φ₃ : MvPowerSeries σ R) :
        φ₁ * φ₂ * φ₃ = φ₁ * (φ₂ * φ₃)
        instance MvPowerSeries.instSemiring {σ : Type u_1} {R : Type u_2} [Semiring R] :
        Equations
        • MvPowerSeries.instSemiring = Semiring.mk npowRecAuto
        Equations
        instance MvPowerSeries.instRing {σ : Type u_1} {R : Type u_2} [Ring R] :
        Equations
        • MvPowerSeries.instRing = Ring.mk SubNegMonoid.zsmul
        instance MvPowerSeries.instCommRing {σ : Type u_1} {R : Type u_2} [CommRing R] :
        Equations
        theorem MvPowerSeries.monomial_mul_monomial {σ : Type u_1} {R : Type u_2} [Semiring R] (m : σ →₀ ) (n : σ →₀ ) (a : R) (b : R) :
        def MvPowerSeries.C (σ : Type u_1) (R : Type u_2) [Semiring R] :

        The constant multivariate formal power series.

        Equations
        Instances For
          @[simp]
          theorem MvPowerSeries.monomial_zero_eq_C {σ : Type u_1} {R : Type u_2} [Semiring R] :
          theorem MvPowerSeries.coeff_C {σ : Type u_1} {R : Type u_2} [Semiring R] [DecidableEq σ] (n : σ →₀ ) (a : R) :
          (MvPowerSeries.coeff R n) ((MvPowerSeries.C σ R) a) = if n = 0 then a else 0
          theorem MvPowerSeries.coeff_zero_C {σ : Type u_1} {R : Type u_2} [Semiring R] (a : R) :
          def MvPowerSeries.X {σ : Type u_1} {R : Type u_2} [Semiring R] (s : σ) :

          The variables of the multivariate formal power series ring.

          Equations
          Instances For
            theorem MvPowerSeries.coeff_X {σ : Type u_1} {R : Type u_2} [Semiring R] [DecidableEq σ] (n : σ →₀ ) (s : σ) :
            (MvPowerSeries.coeff R n) (MvPowerSeries.X s) = if n = Finsupp.single s 1 then 1 else 0
            theorem MvPowerSeries.coeff_index_single_X {σ : Type u_1} {R : Type u_2} [Semiring R] [DecidableEq σ] (s : σ) (t : σ) :
            (MvPowerSeries.coeff R (Finsupp.single t 1)) (MvPowerSeries.X s) = if t = s then 1 else 0
            @[simp]
            theorem MvPowerSeries.coeff_zero_X {σ : Type u_1} {R : Type u_2} [Semiring R] (s : σ) :
            theorem MvPowerSeries.commute_X {σ : Type u_1} {R : Type u_2} [Semiring R] (φ : MvPowerSeries σ R) (s : σ) :
            theorem MvPowerSeries.X_def {σ : Type u_1} {R : Type u_2} [Semiring R] (s : σ) :
            theorem MvPowerSeries.X_pow_eq {σ : Type u_1} {R : Type u_2} [Semiring R] (s : σ) (n : ) :
            theorem MvPowerSeries.coeff_X_pow {σ : Type u_1} {R : Type u_2} [Semiring R] [DecidableEq σ] (m : σ →₀ ) (s : σ) (n : ) :
            (MvPowerSeries.coeff R m) (MvPowerSeries.X s ^ n) = if m = Finsupp.single s n then 1 else 0
            @[simp]
            theorem MvPowerSeries.coeff_mul_C {σ : Type u_1} {R : Type u_2} [Semiring R] (n : σ →₀ ) (φ : MvPowerSeries σ R) (a : R) :
            @[simp]
            theorem MvPowerSeries.coeff_C_mul {σ : Type u_1} {R : Type u_2} [Semiring R] (n : σ →₀ ) (φ : MvPowerSeries σ R) (a : R) :
            theorem MvPowerSeries.coeff_zero_mul_X {σ : Type u_1} {R : Type u_2} [Semiring R] (φ : MvPowerSeries σ R) (s : σ) :
            theorem MvPowerSeries.coeff_zero_X_mul {σ : Type u_1} {R : Type u_2} [Semiring R] (φ : MvPowerSeries σ R) (s : σ) :
            def MvPowerSeries.constantCoeff (σ : Type u_1) (R : Type u_2) [Semiring R] :

            The constant coefficient of a formal power series.

            Equations
            Instances For
              @[simp]
              theorem MvPowerSeries.constantCoeff_C {σ : Type u_1} {R : Type u_2} [Semiring R] (a : R) :
              @[simp]
              @[simp]
              theorem MvPowerSeries.constantCoeff_one {σ : Type u_1} {R : Type u_2} [Semiring R] :
              @[simp]
              theorem MvPowerSeries.constantCoeff_X {σ : Type u_1} {R : Type u_2} [Semiring R] (s : σ) :
              theorem MvPowerSeries.isUnit_constantCoeff {σ : Type u_1} {R : Type u_2} [Semiring R] (φ : MvPowerSeries σ R) (h : IsUnit φ) :

              If a multivariate formal power series is invertible, then so is its constant coefficient.

              @[simp]
              theorem MvPowerSeries.coeff_smul {σ : Type u_1} {R : Type u_2} [Semiring R] (f : MvPowerSeries σ R) (n : σ →₀ ) (a : R) :
              theorem MvPowerSeries.smul_eq_C_mul {σ : Type u_1} {R : Type u_2} [Semiring R] (f : MvPowerSeries σ R) (a : R) :
              a f = (MvPowerSeries.C σ R) a * f
              theorem MvPowerSeries.X_inj {σ : Type u_1} {R : Type u_2} [Semiring R] [Nontrivial R] {s : σ} {t : σ} :
              def MvPowerSeries.map (σ : Type u_1) {R : Type u_2} {S : Type u_3} [Semiring R] [Semiring S] (f : R →+* S) :

              The map between multivariate formal power series induced by a map on the coefficients.

              Equations
              Instances For
                @[simp]
                theorem MvPowerSeries.map_comp {σ : Type u_1} {R : Type u_2} {S : Type u_3} {T : Type u_4} [Semiring R] [Semiring S] [Semiring T] (f : R →+* S) (g : S →+* T) :
                MvPowerSeries.map σ (g.comp f) = (MvPowerSeries.map σ g).comp (MvPowerSeries.map σ f)
                @[simp]
                theorem MvPowerSeries.coeff_map {σ : Type u_1} {R : Type u_2} {S : Type u_3} [Semiring R] [Semiring S] (f : R →+* S) (n : σ →₀ ) (φ : MvPowerSeries σ R) :
                @[simp]
                theorem MvPowerSeries.constantCoeff_map {σ : Type u_1} {R : Type u_2} {S : Type u_3} [Semiring R] [Semiring S] (f : R →+* S) (φ : MvPowerSeries σ R) :
                @[simp]
                theorem MvPowerSeries.map_monomial {σ : Type u_1} {R : Type u_2} {S : Type u_3} [Semiring R] [Semiring S] (f : R →+* S) (n : σ →₀ ) (a : R) :
                @[simp]
                theorem MvPowerSeries.map_C {σ : Type u_1} {R : Type u_2} {S : Type u_3} [Semiring R] [Semiring S] (f : R →+* S) (a : R) :
                (MvPowerSeries.map σ f) ((MvPowerSeries.C σ R) a) = (MvPowerSeries.C σ S) (f a)
                @[simp]
                theorem MvPowerSeries.map_X {σ : Type u_1} {R : Type u_2} {S : Type u_3} [Semiring R] [Semiring S] (f : R →+* S) (s : σ) :
                theorem MvPowerSeries.X_pow_dvd_iff {σ : Type u_1} {R : Type u_2} [Semiring R] {s : σ} {n : } {φ : MvPowerSeries σ R} :
                MvPowerSeries.X s ^ n φ ∀ (m : σ →₀ ), m s < n(MvPowerSeries.coeff R m) φ = 0
                theorem MvPowerSeries.X_dvd_iff {σ : Type u_1} {R : Type u_2} [Semiring R] {s : σ} {φ : MvPowerSeries σ R} :
                MvPowerSeries.X s φ ∀ (m : σ →₀ ), m s = 0(MvPowerSeries.coeff R m) φ = 0
                theorem MvPowerSeries.coeff_prod {σ : Type u_1} {R : Type u_3} [CommSemiring R] {ι : Type u_4} [DecidableEq ι] [DecidableEq σ] (f : ιMvPowerSeries σ R) (d : σ →₀ ) (s : Finset ι) :
                (MvPowerSeries.coeff R d) (∏ js, f j) = ls.finsuppAntidiag d, is, (MvPowerSeries.coeff R (l i)) (f i)

                Coefficients of a product of power series

                theorem MvPowerSeries.coeff_pow {σ : Type u_1} {R : Type u_3} [CommSemiring R] [DecidableEq σ] (f : MvPowerSeries σ R) {n : } (d : σ →₀ ) :
                (MvPowerSeries.coeff R d) (f ^ n) = l(Finset.range n).finsuppAntidiag d, iFinset.range n, (MvPowerSeries.coeff R (l i)) f

                The dth coefficient of a power of a multivariate power series is the sum, indexed by finsuppAntidiag (Finset.range n) d, of products of coefficients

                theorem MvPowerSeries.coeff_eq_zero_of_constantCoeff_nilpotent {σ : Type u_1} {R : Type u_3} [CommSemiring R] {f : MvPowerSeries σ R} {m : } (hf : (MvPowerSeries.constantCoeff σ R) f ^ m = 0) {d : σ →₀ } {n : } (hn : m + d.degree n) :
                (MvPowerSeries.coeff R d) (f ^ n) = 0

                Vanishing of coefficients of powers of multivariate power series when the constant coefficient is nilpotent [N. Bourbaki, Algebra {II}, Chapter 4, §4, n°2, proposition 3][bourbaki1981]

                instance MvPowerSeries.instAlgebra {σ : Type u_1} {R : Type u_2} {A : Type u_3} [CommSemiring R] [Semiring A] [Algebra R A] :
                Equations
                theorem MvPowerSeries.algebraMap_apply {σ : Type u_1} {R : Type u_2} {A : Type u_3} [CommSemiring R] [Semiring A] [Algebra R A] {r : R} :
                (algebraMap R (MvPowerSeries σ A)) r = (MvPowerSeries.C σ A) ((algebraMap R A) r)
                def MvPolynomial.toMvPowerSeries {σ : Type u_1} {R : Type u_2} [CommSemiring R] :

                The natural inclusion from multivariate polynomials into multivariate formal power series.

                Equations
                Instances For
                  instance MvPolynomial.coeToMvPowerSeries {σ : Type u_1} {R : Type u_2} [CommSemiring R] :

                  The natural inclusion from multivariate polynomials into multivariate formal power series.

                  Equations
                  • MvPolynomial.coeToMvPowerSeries = { coe := MvPolynomial.toMvPowerSeries }
                  theorem MvPolynomial.coe_def {σ : Type u_1} {R : Type u_2} [CommSemiring R] (φ : MvPolynomial σ R) :
                  φ = fun (n : σ →₀ ) => MvPolynomial.coeff n φ
                  @[simp]
                  theorem MvPolynomial.coeff_coe {σ : Type u_1} {R : Type u_2} [CommSemiring R] (φ : MvPolynomial σ R) (n : σ →₀ ) :
                  @[simp]
                  theorem MvPolynomial.coe_monomial {σ : Type u_1} {R : Type u_2} [CommSemiring R] (n : σ →₀ ) (a : R) :
                  @[simp]
                  theorem MvPolynomial.coe_zero {σ : Type u_1} {R : Type u_2} [CommSemiring R] :
                  0 = 0
                  @[simp]
                  theorem MvPolynomial.coe_one {σ : Type u_1} {R : Type u_2} [CommSemiring R] :
                  1 = 1
                  @[simp]
                  theorem MvPolynomial.coe_add {σ : Type u_1} {R : Type u_2} [CommSemiring R] (φ : MvPolynomial σ R) (ψ : MvPolynomial σ R) :
                  (φ + ψ) = φ + ψ
                  @[simp]
                  theorem MvPolynomial.coe_mul {σ : Type u_1} {R : Type u_2} [CommSemiring R] (φ : MvPolynomial σ R) (ψ : MvPolynomial σ R) :
                  (φ * ψ) = φ * ψ
                  @[simp]
                  theorem MvPolynomial.coe_C {σ : Type u_1} {R : Type u_2} [CommSemiring R] (a : R) :
                  (MvPolynomial.C a) = (MvPowerSeries.C σ R) a
                  @[simp]
                  theorem MvPolynomial.coe_X {σ : Type u_1} {R : Type u_2} [CommSemiring R] (s : σ) :
                  @[simp]
                  theorem MvPolynomial.coe_inj {σ : Type u_1} {R : Type u_2} [CommSemiring R] {φ : MvPolynomial σ R} {ψ : MvPolynomial σ R} :
                  φ = ψ φ = ψ
                  @[simp]
                  theorem MvPolynomial.coe_eq_zero_iff {σ : Type u_1} {R : Type u_2} [CommSemiring R] {φ : MvPolynomial σ R} :
                  φ = 0 φ = 0
                  @[simp]
                  theorem MvPolynomial.coe_eq_one_iff {σ : Type u_1} {R : Type u_2} [CommSemiring R] {φ : MvPolynomial σ R} :
                  φ = 1 φ = 1

                  The coercion from multivariate polynomials to multivariate power series as a ring homomorphism.

                  Equations
                  • MvPolynomial.coeToMvPowerSeries.ringHom = { toFun := Coe.coe, map_one' := , map_mul' := , map_zero' := , map_add' := }
                  Instances For
                    @[simp]
                    theorem MvPolynomial.coe_pow {σ : Type u_1} {R : Type u_2} [CommSemiring R] {φ : MvPolynomial σ R} (n : ) :
                    (φ ^ n) = φ ^ n
                    @[simp]
                    theorem MvPolynomial.coeToMvPowerSeries.ringHom_apply {σ : Type u_1} {R : Type u_2} [CommSemiring R] (φ : MvPolynomial σ R) :
                    MvPolynomial.coeToMvPowerSeries.ringHom φ = φ

                    The coercion from multivariate polynomials to multivariate power series as an algebra homomorphism.

                    Equations
                    Instances For
                      instance MvPowerSeries.algebraMvPolynomial {σ : Type u_1} {R : Type u_2} {A : Type u_3} [CommSemiring R] [CommSemiring A] [Algebra R A] :
                      Equations
                      instance MvPowerSeries.algebraMvPowerSeries {σ : Type u_1} {R : Type u_2} {A : Type u_3} [CommSemiring R] [CommSemiring A] [Algebra R A] :
                      Equations
                      theorem MvPowerSeries.algebraMap_apply' {σ : Type u_1} {R : Type u_2} (A : Type u_3) [CommSemiring R] [CommSemiring A] [Algebra R A] (p : MvPolynomial σ R) :
                      theorem MvPowerSeries.algebraMap_apply'' {σ : Type u_1} {R : Type u_2} (A : Type u_3) [CommSemiring R] [CommSemiring A] [Algebra R A] (f : MvPowerSeries σ R) :