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.

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 (max u_2 u_1) 0)

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

Equations

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

Instances For

instance MvPowerSeries.instInhabitedMvPowerSeries {σ : Type u_1} {R : Type u_2} [Inhabited R] :

Inhabited (MvPowerSeries σ R)

Equations

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

instance MvPowerSeries.instZeroMvPowerSeries {σ : Type u_1} {R : Type u_2} [Zero R] :

Zero (MvPowerSeries σ R)

Equations

MvPowerSeries.instZeroMvPowerSeries = Pi.instZero

instance MvPowerSeries.instAddMonoidMvPowerSeries {σ : Type u_1} {R : Type u_2} [AddMonoid R] :

AddMonoid (MvPowerSeries σ R)

Equations

MvPowerSeries.instAddMonoidMvPowerSeries = Pi.addMonoid

instance MvPowerSeries.instAddGroupMvPowerSeries {σ : Type u_1} {R : Type u_2} [AddGroup R] :

AddGroup (MvPowerSeries σ R)

Equations

MvPowerSeries.instAddGroupMvPowerSeries = Pi.addGroup

instance MvPowerSeries.instAddCommMonoidMvPowerSeries {σ : Type u_1} {R : Type u_2} [AddCommMonoid R] :

AddCommMonoid (MvPowerSeries σ R)

Equations

MvPowerSeries.instAddCommMonoidMvPowerSeries = Pi.addCommMonoid

instance MvPowerSeries.instAddCommGroupMvPowerSeries {σ : Type u_1} {R : Type u_2} [AddCommGroup R] :

AddCommGroup (MvPowerSeries σ R)

Equations

MvPowerSeries.instAddCommGroupMvPowerSeries = Pi.addCommGroup

instance MvPowerSeries.instNontrivialMvPowerSeries {σ : Type u_1} {R : Type u_2} [Nontrivial R] :

Nontrivial (MvPowerSeries σ R)

Equations

⋯ = ⋯

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

Module R (MvPowerSeries σ A)

Equations

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

instance MvPowerSeries.instIsScalarTowerMvPowerSeriesToSMulInstZeroMvPowerSeriesToZeroToAddMonoidToSMulZeroClassToZeroToMonoidWithZeroToSMulWithZeroToMulActionWithZeroInstAddCommMonoidMvPowerSeriesInstModuleMvPowerSeriesInstAddCommMonoidMvPowerSeriesToSMulToSMulZeroClassToZeroToMonoidWithZeroToSMulWithZeroToMulActionWithZeroInstModuleMvPowerSeriesInstAddCommMonoidMvPowerSeries {σ : 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.stdBasis R (fun (x : σ →₀ ℕ) => R) n

Instances For

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

Instances For

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.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.monomial_def {σ : Type u_1} {R : Type u_2} [Semiring R] [DecidableEq σ] (n : σ →₀ ℕ) :

MvPowerSeries.monomial R n = LinearMap.stdBasis 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

theorem MvPowerSeries.coeff_zero {σ : Type u_1} {R : Type u_2} [Semiring R] (n : σ →₀ ℕ) :

(MvPowerSeries.coeff R n) 0 = 0

instance MvPowerSeries.instOneMvPowerSeries {σ : Type u_1} {R : Type u_2} [Semiring R] :

One (MvPowerSeries σ R)

Equations

MvPowerSeries.instOneMvPowerSeries = { 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.instAddMonoidWithOneMvPowerSeries {σ : Type u_1} {R : Type u_2} [Semiring R] :

AddMonoidWithOne (MvPowerSeries σ R)

Equations

MvPowerSeries.instAddMonoidWithOneMvPowerSeries = let __src := let_fun this := inferInstance; this; AddMonoidWithOne.mk ⋯ ⋯

instance MvPowerSeries.instMulMvPowerSeries {σ : Type u_1} {R : Type u_2} [Semiring R] :

Mul (MvPowerSeries σ R)

Equations

One or more equations did not get rendered due to their size.

theorem MvPowerSeries.coeff_mul {σ : Type u_1} {R : Type u_2} [Semiring R] (n : σ →₀ ℕ) (φ : MvPowerSeries σ R) (ψ : MvPowerSeries σ R) [DecidableEq σ] :

(MvPowerSeries.coeff R n) (φ * ψ) = Finset.sum (Finset.antidiagonal n) fun (p : (σ →₀ ℕ) × (σ →₀ ℕ)) => (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) (φ₂ : 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.instSemiringMvPowerSeries {σ : Type u_1} {R : Type u_2} [Semiring R] :

Semiring (MvPowerSeries σ R)

Equations

One or more equations did not get rendered due to their size.

instance MvPowerSeries.instCommSemiringMvPowerSeries {σ : Type u_1} {R : Type u_2} [CommSemiring R] :

CommSemiring (MvPowerSeries σ R)

Equations

MvPowerSeries.instCommSemiringMvPowerSeries = let __src := let_fun this := inferInstance; this; CommSemiring.mk ⋯

instance MvPowerSeries.instRingMvPowerSeries {σ : Type u_1} {R : Type u_2} [Ring R] :

Ring (MvPowerSeries σ R)

Equations

One or more equations did not get rendered due to their size.

instance MvPowerSeries.instCommRingMvPowerSeries {σ : Type u_1} {R : Type u_2} [CommRing R] :

CommRing (MvPowerSeries σ R)

Equations

MvPowerSeries.instCommRingMvPowerSeries = let __src := inferInstanceAs (CommSemiring (MvPowerSeries σ R)); let __src_1 := inferInstanceAs (AddCommGroup (MvPowerSeries σ R)); CommRing.mk ⋯

theorem MvPowerSeries.monomial_mul_monomial {σ : Type u_1} {R : Type u_2} [Semiring R] (m : σ →₀ ℕ) (n : σ →₀ ℕ) (a : R) (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 = let __src := MvPowerSeries.monomial R 0; { toMonoidHom := { toOneHom := { toFun := __src.toFun, map_one' := ⋯ }, map_mul' := ⋯ }, map_zero' := ⋯, map_add' := ⋯ }

Instances For

@[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

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_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

One or more equations did not get rendered due to their size.

Instances For

@[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] :

RingHom.comp (MvPowerSeries.constantCoeff σ R) (MvPowerSeries.C σ R) = RingHom.id R

theorem MvPowerSeries.constantCoeff_zero {σ : Type u_1} {R : Type u_2} [Semiring R] :

(MvPowerSeries.constantCoeff σ R) 0 = 0

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.

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

One or more equations did not get rendered due to their size.

Instances For

@[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 σ (RingHom.comp g f) = RingHom.comp (MvPowerSeries.map σ g) (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) (Finset.prod s fun (j : ι) => f j) = Finset.sum (Finset.piAntidiagonal s d) fun (l : ι →₀ σ →₀ ℕ) => Finset.prod s fun (i : ι) => (MvPowerSeries.coeff R (l i)) (f i)

Coefficients of a product of power series

instance MvPowerSeries.instAlgebraMvPowerSeriesInstSemiringMvPowerSeries {σ : Type u_1} {R : Type u_2} {A : Type u_3} [CommSemiring R] [Semiring A] [Algebra R A] :

Algebra R (MvPowerSeries σ A)

Equations

One or more equations did not get rendered due to their size.

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.instNontrivialSubalgebraMvPowerSeriesInstSemiringMvPowerSeriesToSemiringInstAlgebraMvPowerSeriesInstSemiringMvPowerSeriesId {σ : 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 φ

Instances For

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) (ψ : 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_bit0 {σ : Type u_1} {R : Type u_2} [CommSemiring R] (φ : MvPolynomial σ R) :

↑(bit0 φ) = bit0 ↑φ

@[simp]

theorem MvPolynomial.coe_bit1 {σ : Type u_1} {R : Type u_2} [CommSemiring R] (φ : MvPolynomial σ R) :

↑(bit1 φ) = bit1 ↑φ

@[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} {ψ : 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 = { toMonoidHom := { toOneHom := { 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 φ = ↑φ

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 = let __src := RingHom.comp (MvPowerSeries.map σ (algebraMap R A)) MvPolynomial.coeToMvPowerSeries.ringHom; { toRingHom := __src, commutes' := ⋯ }

Instances For

@[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 = RingHom.toAlgebra (MvPolynomial.coeToMvPowerSeries.algHom A).toRingHom

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

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