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

• MvPowerSeries.C: constant power series

• MvPowerSeries.X: the indeterminates

• MvPowerSeries.coeff, MvPowerSeries.constantCoeff: the coefficients of a MvPowerSeries, its constant coefficient

• MvPowerSeries.monomial: the monomials

• MvPowerSeries.coeff_mul: computes the coefficients of the product of two MvPowerSeries

• MvPowerSeries.coeff_prod : computes the coefficients of products of MvPowerSeries

• MvPowerSeries.coeff_pow : computes the coefficients of powers of a MvPowerSeries

• MvPowerSeries.coeff_eq_zero_of_constantCoeff_nilpotent: if the constant coefficient of a MvPowerSeries is nilpotent, then some coefficients of its powers are automatically zero

• MvPowerSeries.map: apply a RingHom to the coefficients of a MvPowerSeries (as a `RingHom)

• MvPowerSeries.X_pow_dvd_iff, MvPowerSeries.X_dvd_iff: equivalent conditions for (a power of) an indeterminate to divide a MvPowerSeries

• MvPolynomial.toMvPowerSeries: the canonical coercion from MvPolynomial to MvPowerSeries

Note

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

• Mathlib.RingTheory.MvPowerSeries.Inverse : invertibility, formal power series over a local ring form a local ring;
• Mathlib.RingTheory.MvPowerSeries.Trunc: truncation of power series.

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 u_2 u_1)

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

Equations

• MvPowerSeries σ R = ((σ →₀ ℕ) → R)

instance MvPowerSeries.instInhabited {σ : Type u_1} {R : Type u_2} [Inhabited R] : Inhabited (MvPowerSeries σ R)

Equations

• MvPowerSeries.instInhabited = { default := fun (x : σ →₀ ℕ) => default }

instance MvPowerSeries.instZero {σ : Type u_1} {R : Type u_2} [Zero R] : Zero (MvPowerSeries σ R)

Equations

• MvPowerSeries.instZero = Pi.instZero

instance MvPowerSeries.instAddMonoid {σ : Type u_1} {R : Type u_2} [AddMonoid R] : AddMonoid (MvPowerSeries σ R)

Equations

• MvPowerSeries.instAddMonoid = Pi.addMonoid

instance MvPowerSeries.instAddGroup {σ : Type u_1} {R : Type u_2} [AddGroup R] : AddGroup (MvPowerSeries σ R)

Equations

• MvPowerSeries.instAddGroup = Pi.addGroup

instance MvPowerSeries.instAddCommMonoid {σ : Type u_1} {R : Type u_2} [AddCommMonoid R] : AddCommMonoid (MvPowerSeries σ R)

Equations

• MvPowerSeries.instAddCommMonoid = Pi.addCommMonoid

instance MvPowerSeries.instAddCommGroup {σ : Type u_1} {R : Type u_2} [AddCommGroup R] : AddCommGroup (MvPowerSeries σ R)

Equations

• MvPowerSeries.instAddCommGroup = Pi.addCommGroup

instance MvPowerSeries.instNontrivial {σ : Type u_1} {R : Type u_2} [Nontrivial R] : Nontrivial (MvPowerSeries σ R)

Equations

• ⋯ = ⋯

instance MvPowerSeries.instModule {σ : Type u_1} {R : Type u_2} {A : Type u_3} [Semiring R] [AddCommMonoid A] [Module R A] : Module R (MvPowerSeries σ A)

Equations

• MvPowerSeries.instModule = Pi.module (σ →₀ ℕ) (fun (a : σ →₀ ℕ) => A) R

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] : IsScalarTower R S (MvPowerSeries σ A)

Equations

• ⋯ = ⋯

def MvPowerSeries.monomial {σ : Type u_1} (R : Type u_2) [Semiring R] (n : σ →₀ ℕ) : R →ₗ[R] MvPowerSeries σ R

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

• MvPowerSeries.monomial R n = LinearMap.single R (fun (x : σ →₀ ℕ) => R) n

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

The nth coefficient of a multivariate formal power series.

Equations

• MvPowerSeries.coeff R n = LinearMap.proj n

theorem MvPowerSeries.coeff_apply {σ : Type u_1} (R : Type u_2) [Semiring R] (f : MvPowerSeries σ R) (d : σ →₀ ℕ) : (MvPowerSeries.coeff R d) f = f d

theorem MvPowerSeries.ext {σ : Type u_1} {R : Type u_2} [Semiring 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.ext_iff {σ : Type u_1} {R : Type u_2} [Semiring 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.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) : (MvPowerSeries.coeff R n) ((MvPowerSeries.monomial R n) a) = a

theorem MvPowerSeries.coeff_monomial_ne {σ : Type u_1} {R : Type u_2} [Semiring R] {m n : σ →₀ ℕ} (h : m ≠ n) (a : R) : (MvPowerSeries.coeff R m) ((MvPowerSeries.monomial R n) a) = 0

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 : σ →₀ ℕ) : (MvPowerSeries.coeff R n) 0 = 0

theorem MvPowerSeries.eq_zero_iff_forall_coeff_zero {σ : Type u_1} {R : Type u_2} [Semiring R] {f : MvPowerSeries σ R} : f = 0 ↔ ∀ (d : σ →₀ ℕ), (MvPowerSeries.coeff R d) f = 0

theorem MvPowerSeries.ne_zero_iff_exists_coeff_ne_zero {σ : Type u_1} {R : Type u_2} [Semiring R] (f : MvPowerSeries σ R) : f ≠ 0 ↔ ∃ (d : σ →₀ ℕ), (MvPowerSeries.coeff R d) f ≠ 0

instance MvPowerSeries.instOne {σ : Type u_1} {R : Type u_2} [Semiring R] : One (MvPowerSeries σ R)

Equations

• MvPowerSeries.instOne = { one := (MvPowerSeries.monomial R 0) 1 }

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] : (MvPowerSeries.coeff R 0) 1 = 1

theorem MvPowerSeries.monomial_zero_one {σ : Type u_1} {R : Type u_2} [Semiring R] : (MvPowerSeries.monomial R 0) 1 = 1

instance MvPowerSeries.instAddMonoidWithOne {σ : Type u_1} {R : Type u_2} [Semiring R] : AddMonoidWithOne (MvPowerSeries σ R)

Equations

• MvPowerSeries.instAddMonoidWithOne = AddMonoidWithOne.mk ⋯ ⋯

instance MvPowerSeries.instMul {σ : Type u_1} {R : Type u_2} [Semiring R] : Mul (MvPowerSeries σ R)

Equations

• MvPowerSeries.instMul = { mul := fun (φ ψ : MvPowerSeries σ R) (n : σ →₀ ℕ) => ∑ p ∈ Finset.antidiagonal n, (MvPowerSeries.coeff R p.1) φ * (MvPowerSeries.coeff R p.2) ψ }

theorem MvPowerSeries.coeff_mul {σ : Type u_1} {R : Type u_2} [Semiring R] (n : σ →₀ ℕ) (φ ψ : MvPowerSeries σ R) [DecidableEq σ] : (MvPowerSeries.coeff R n) (φ * ψ) = ∑ p ∈ Finset.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) : (MvPowerSeries.coeff R (m + n)) ((MvPowerSeries.monomial R m) a * φ) = a * (MvPowerSeries.coeff R n) φ

theorem MvPowerSeries.coeff_add_mul_monomial {σ : Type u_1} {R : Type u_2} [Semiring R] (m n : σ →₀ ℕ) (φ : MvPowerSeries σ R) (a : R) : (MvPowerSeries.coeff R (m + n)) (φ * (MvPowerSeries.monomial R n) a) = (MvPowerSeries.coeff R m) φ * a

@[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) : φ₁ * (φ₂ + φ₃) = φ₁ * φ₂ + φ₁ * φ₃

theorem MvPowerSeries.add_mul {σ : Type u_1} {R : Type u_2} [Semiring R] (φ₁ φ₂ φ₃ : MvPowerSeries σ R) : (φ₁ + φ₂) * φ₃ = φ₁ * φ₃ + φ₂ * φ₃

theorem MvPowerSeries.mul_assoc {σ : Type u_1} {R : Type u_2} [Semiring R] (φ₁ φ₂ φ₃ : MvPowerSeries σ R) : φ₁ * φ₂ * φ₃ = φ₁ * (φ₂ * φ₃)

instance MvPowerSeries.instSemiring {σ : Type u_1} {R : Type u_2} [Semiring R] : Semiring (MvPowerSeries σ R)

Equations

• MvPowerSeries.instSemiring = Semiring.mk ⋯ ⋯ ⋯ ⋯ npowRecAuto ⋯ ⋯

instance MvPowerSeries.instCommSemiring {σ : Type u_1} {R : Type u_2} [CommSemiring R] : CommSemiring (MvPowerSeries σ R)

Equations

• MvPowerSeries.instCommSemiring = CommSemiring.mk ⋯

instance MvPowerSeries.instRing {σ : Type u_1} {R : Type u_2} [Ring R] : Ring (MvPowerSeries σ R)

Equations

• MvPowerSeries.instRing = Ring.mk ⋯ SubNegMonoid.zsmul ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

instance MvPowerSeries.instCommRing {σ : Type u_1} {R : Type u_2} [CommRing R] : CommRing (MvPowerSeries σ R)

Equations

• MvPowerSeries.instCommRing = CommRing.mk ⋯

theorem MvPowerSeries.monomial_mul_monomial {σ : Type u_1} {R : Type u_2} [Semiring R] (m n : σ →₀ ℕ) (a b : R) : (MvPowerSeries.monomial R m) a * (MvPowerSeries.monomial R n) b = (MvPowerSeries.monomial R (m + n)) (a * b)

def MvPowerSeries.C (σ : Type u_1) (R : Type u_2) [Semiring R] : R →+* MvPowerSeries σ R

The constant multivariate formal power series.

Equations

• MvPowerSeries.C σ R = { toFun := (MvPowerSeries.monomial R 0).toFun, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }

@[simp]

theorem MvPowerSeries.monomial_zero_eq_C {σ : Type u_1} {R : Type u_2} [Semiring R] : ⇑(MvPowerSeries.monomial R 0) = ⇑(MvPowerSeries.C σ R)

theorem MvPowerSeries.monomial_zero_eq_C_apply {σ : Type u_1} {R : Type u_2} [Semiring R] (a : R) : (MvPowerSeries.monomial R 0) a = (MvPowerSeries.C σ R) a

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) : (MvPowerSeries.coeff R 0) ((MvPowerSeries.C σ R) a) = a

def MvPowerSeries.X {σ : Type u_1} {R : Type u_2} [Semiring R] (s : σ) : MvPowerSeries σ R

The variables of the multivariate formal power series ring.

Equations

• MvPowerSeries.X s = (MvPowerSeries.monomial R (Finsupp.single s 1)) 1

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_index_single_self_X {σ : Type u_1} {R : Type u_2} [Semiring R] (s : σ) : (MvPowerSeries.coeff R (Finsupp.single s 1)) (MvPowerSeries.X s) = 1

theorem MvPowerSeries.coeff_zero_X {σ : Type u_1} {R : Type u_2} [Semiring R] (s : σ) : (MvPowerSeries.coeff R 0) (MvPowerSeries.X s) = 0

theorem MvPowerSeries.commute_X {σ : Type u_1} {R : Type u_2} [Semiring R] (φ : MvPowerSeries σ R) (s : σ) : Commute φ (MvPowerSeries.X s)

theorem MvPowerSeries.X_def {σ : Type u_1} {R : Type u_2} [Semiring R] (s : σ) : MvPowerSeries.X s = (MvPowerSeries.monomial R (Finsupp.single s 1)) 1

theorem MvPowerSeries.X_pow_eq {σ : Type u_1} {R : Type u_2} [Semiring R] (s : σ) (n : ℕ) : MvPowerSeries.X s ^ n = (MvPowerSeries.monomial R (Finsupp.single s n)) 1

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) : (MvPowerSeries.coeff R n) (φ * (MvPowerSeries.C σ R) a) = (MvPowerSeries.coeff R n) φ * a

@[simp]

theorem MvPowerSeries.coeff_C_mul {σ : Type u_1} {R : Type u_2} [Semiring R] (n : σ →₀ ℕ) (φ : MvPowerSeries σ R) (a : R) : (MvPowerSeries.coeff R n) ((MvPowerSeries.C σ R) a * φ) = a * (MvPowerSeries.coeff R n) φ

theorem MvPowerSeries.coeff_zero_mul_X {σ : Type u_1} {R : Type u_2} [Semiring R] (φ : MvPowerSeries σ R) (s : σ) : (MvPowerSeries.coeff R 0) (φ * MvPowerSeries.X s) = 0

theorem MvPowerSeries.coeff_zero_X_mul {σ : Type u_1} {R : Type u_2} [Semiring R] (φ : MvPowerSeries σ R) (s : σ) : (MvPowerSeries.coeff R 0) (MvPowerSeries.X s * φ) = 0

def MvPowerSeries.constantCoeff (σ : Type u_1) (R : Type u_2) [Semiring R] : MvPowerSeries σ R →+* R

The constant coefficient of a formal power series.

Equations

• MvPowerSeries.constantCoeff σ R = { toFun := ⇑(MvPowerSeries.coeff R 0), map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }

@[simp]

theorem MvPowerSeries.coeff_zero_eq_constantCoeff {σ : Type u_1} {R : Type u_2} [Semiring R] : ⇑(MvPowerSeries.coeff R 0) = ⇑(MvPowerSeries.constantCoeff σ R)

theorem MvPowerSeries.coeff_zero_eq_constantCoeff_apply {σ : Type u_1} {R : Type u_2} [Semiring R] (φ : MvPowerSeries σ R) : (MvPowerSeries.coeff R 0) φ = (MvPowerSeries.constantCoeff σ R) φ

@[simp]

theorem MvPowerSeries.constantCoeff_C {σ : Type u_1} {R : Type u_2} [Semiring R] (a : R) : (MvPowerSeries.constantCoeff σ R) ((MvPowerSeries.C σ R) a) = a

@[simp]

theorem MvPowerSeries.constantCoeff_comp_C {σ : Type u_1} {R : Type u_2} [Semiring R] : (MvPowerSeries.constantCoeff σ R).comp (MvPowerSeries.C σ R) = RingHom.id R

@[simp]

theorem MvPowerSeries.constantCoeff_zero {σ : Type u_1} {R : Type u_2} [Semiring R] : (MvPowerSeries.constantCoeff σ R) 0 = 0

@[simp]

theorem MvPowerSeries.constantCoeff_one {σ : Type u_1} {R : Type u_2} [Semiring R] : (MvPowerSeries.constantCoeff σ R) 1 = 1

@[simp]

theorem MvPowerSeries.constantCoeff_X {σ : Type u_1} {R : Type u_2} [Semiring R] (s : σ) : (MvPowerSeries.constantCoeff σ R) (MvPowerSeries.X s) = 0

theorem MvPowerSeries.isUnit_constantCoeff {σ : Type u_1} {R : Type u_2} [Semiring R] (φ : MvPowerSeries σ R) (h : IsUnit φ) : IsUnit ((MvPowerSeries.constantCoeff σ R) φ)

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) : (MvPowerSeries.coeff R n) (a • f) = a * (MvPowerSeries.coeff R n) f

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 : σ} : MvPowerSeries.X s = MvPowerSeries.X t ↔ s = t

def MvPowerSeries.map (σ : Type u_1) {R : Type u_2} {S : Type u_3} [Semiring R] [Semiring S] (f : R →+* S) : MvPowerSeries σ R →+* MvPowerSeries σ S

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

Equations

• MvPowerSeries.map σ f = { toFun := fun (φ : MvPowerSeries σ R) (n : σ →₀ ℕ) => f ((MvPowerSeries.coeff R n) φ), map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }

@[simp]

theorem MvPowerSeries.map_id {σ : Type u_1} {R : Type u_2} [Semiring R] : MvPowerSeries.map σ (RingHom.id R) = RingHom.id (MvPowerSeries σ R)

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) : (MvPowerSeries.coeff S n) ((MvPowerSeries.map σ f) φ) = f ((MvPowerSeries.coeff R n) φ)

@[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) : (MvPowerSeries.constantCoeff σ S) ((MvPowerSeries.map σ f) φ) = f ((MvPowerSeries.constantCoeff σ 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) : (MvPowerSeries.map σ f) ((MvPowerSeries.monomial R n) a) = (MvPowerSeries.monomial S n) (f a)

@[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 : σ) : (MvPowerSeries.map σ f) (MvPowerSeries.X s) = MvPowerSeries.X 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) (∏ j ∈ s, f j) = ∑ l ∈ s.finsuppAntidiag d, ∏ i ∈ s, (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, ∏ i ∈ Finset.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] : Algebra R (MvPowerSeries σ A)

Equations

• MvPowerSeries.instAlgebra = Algebra.mk ((MvPowerSeries.map σ (algebraMap R A)).comp (MvPowerSeries.C σ R)) ⋯ ⋯

theorem MvPowerSeries.c_eq_algebraMap {σ : Type u_1} {R : Type u_2} [CommSemiring R] : MvPowerSeries.C σ R = algebraMap R (MvPowerSeries σ R)

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)

instance MvPowerSeries.instNontrivialSubalgebraOfNonempty {σ : Type u_1} {R : Type u_2} [CommSemiring R] [Nonempty σ] [Nontrivial R] : Nontrivial (Subalgebra R (MvPowerSeries σ R))

Equations

• ⋯ = ⋯

def MvPolynomial.toMvPowerSeries {σ : Type u_1} {R : Type u_2} [CommSemiring R] : MvPolynomial σ R → MvPowerSeries σ R

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

Equations

• ↑φ n = MvPolynomial.coeff n φ

instance MvPolynomial.coeToMvPowerSeries {σ : Type u_1} {R : Type u_2} [CommSemiring R] : Coe (MvPolynomial σ R) (MvPowerSeries σ 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 : σ →₀ ℕ) : (MvPowerSeries.coeff R n) ↑φ = MvPolynomial.coeff n φ

@[simp]

theorem MvPolynomial.coe_monomial {σ : Type u_1} {R : Type u_2} [CommSemiring R] (n : σ →₀ ℕ) (a : R) : ↑((MvPolynomial.monomial n) a) = (MvPowerSeries.monomial R n) a

@[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) : ↑(φ + ψ) = ↑φ + ↑ψ

@[simp]

theorem MvPolynomial.coe_mul {σ : Type u_1} {R : Type u_2} [CommSemiring 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 : σ) : ↑(MvPolynomial.X s) = MvPowerSeries.X s

theorem MvPolynomial.coe_injective (σ : Type u_1) (R : Type u_2) [CommSemiring R] : Function.Injective Coe.coe

@[simp]

theorem MvPolynomial.coe_inj {σ : Type u_1} {R : Type u_2} [CommSemiring 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

def MvPolynomial.coeToMvPowerSeries.ringHom {σ : Type u_1} {R : Type u_2} [CommSemiring R] : MvPolynomial σ R →+* MvPowerSeries σ R

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' := ⋯ }

@[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 φ = ↑φ

def MvPolynomial.coeToMvPowerSeries.algHom {σ : Type u_1} {R : Type u_2} [CommSemiring R] (A : Type u_3) [CommSemiring A] [Algebra R A] : MvPolynomial σ R →ₐ[R] MvPowerSeries σ A

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

Equations

• MvPolynomial.coeToMvPowerSeries.algHom A = { toRingHom := (MvPowerSeries.map σ (algebraMap R A)).comp MvPolynomial.coeToMvPowerSeries.ringHom, commutes' := ⋯ }

@[simp]

theorem MvPolynomial.coeToMvPowerSeries.algHom_apply {σ : Type u_1} {R : Type u_2} [CommSemiring R] (φ : MvPolynomial σ R) (A : Type u_3) [CommSemiring A] [Algebra R A] : (MvPolynomial.coeToMvPowerSeries.algHom A) φ = (MvPowerSeries.map σ (algebraMap R A)) ↑φ

instance MvPowerSeries.algebraMvPolynomial {σ : Type u_1} {R : Type u_2} {A : Type u_3} [CommSemiring R] [CommSemiring A] [Algebra R A] : Algebra (MvPolynomial σ R) (MvPowerSeries σ A)

Equations

• MvPowerSeries.algebraMvPolynomial = (MvPolynomial.coeToMvPowerSeries.algHom A).toAlgebra

instance MvPowerSeries.algebraMvPowerSeries {σ : Type u_1} {R : Type u_2} {A : Type u_3} [CommSemiring R] [CommSemiring A] [Algebra R A] : Algebra (MvPowerSeries σ R) (MvPowerSeries σ A)

Equations

• MvPowerSeries.algebraMvPowerSeries = (MvPowerSeries.map σ (algebraMap R A)).toAlgebra

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) : (algebraMap (MvPolynomial σ R) (MvPowerSeries σ A)) p = (MvPowerSeries.map σ (algebraMap R A)) ↑p

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) : (algebraMap (MvPowerSeries σ R) (MvPowerSeries σ A)) f = (MvPowerSeries.map σ (algebraMap R A)) f