Formal 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 polynomials to formal power series.

Generalities

The file starts with setting up the (semi)ring structure on multivariate power series.

trunc n φ truncates a formal power series to the polynomial that has the same coefficients as φ, for all m < n, and 0 otherwise.

If the constant coefficient of a formal power series is invertible, then this formal power series is invertible.

Formal power series over a local ring form a local ring.

Formal power series in one variable

We prove that if the ring of coefficients is an integral domain, then formal power series in one variable form an integral domain.

The order of a formal power series φ is the multiplicity of the variable X in φ.

If the coefficients form an integral domain, then order is a valuation (order_mul, le_order_add).

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.

Formal power series in one variable are defined as PowerSeries R := MvPowerSeries Unit R.

This allows us to port a lot of proofs and properties from the multivariate case to the single variable case. However, it means that formal power series are indexed by Unit →₀ ℕ, which is of course canonically isomorphic to ℕ. We then build some glue to treat formal power series as if they are indexed by ℕ. Occasionally this leads to proofs that are uglier than expected.

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.

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

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

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

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

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

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

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

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)

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)

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

The nth monomial with coefficient a as multivariate formal power series.

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.

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 : σ →₀ ℕ) : LinearMap.comp (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)

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)

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

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 (Finsupp.antidiagonal n) fun p => ↑(MvPowerSeries.coeff R p.fst) φ * ↑(MvPowerSeries.coeff R p.snd) ψ

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)

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

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

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

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.

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

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 = fun₀ | 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 fun₀ | 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 fun₀ | 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 fun₀ | 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 fun₀ | 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 = fun₀ | 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.

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

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

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)

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

def MvPowerSeries.truncFun {σ : Type u_1} {R : Type u_2} [CommSemiring R] (n : σ →₀ ℕ) (φ : MvPowerSeries σ R) : MvPolynomial σ R

Auxiliary definition for the truncation function.

theorem MvPowerSeries.coeff_truncFun {σ : Type u_1} {R : Type u_2} [CommSemiring R] (n : σ →₀ ℕ) (m : σ →₀ ℕ) (φ : MvPowerSeries σ R) : MvPolynomial.coeff m (MvPowerSeries.truncFun n φ) = if m < n then ↑(MvPowerSeries.coeff R m) φ else 0

def MvPowerSeries.trunc {σ : Type u_1} (R : Type u_2) [CommSemiring R] (n : σ →₀ ℕ) : MvPowerSeries σ R →+ MvPolynomial σ R

The nth truncation of a multivariate formal power series to a multivariate polynomial

theorem MvPowerSeries.coeff_trunc {σ : Type u_1} {R : Type u_2} [CommSemiring R] (n : σ →₀ ℕ) (m : σ →₀ ℕ) (φ : MvPowerSeries σ R) : MvPolynomial.coeff m (↑(MvPowerSeries.trunc R n) φ) = if m < n then ↑(MvPowerSeries.coeff R m) φ else 0

@[simp]

theorem MvPowerSeries.trunc_one {σ : Type u_1} {R : Type u_2} [CommSemiring R] (n : σ →₀ ℕ) (hnn : n ≠ 0) : ↑(MvPowerSeries.trunc R n) 1 = 1

@[simp]

theorem MvPowerSeries.trunc_c {σ : Type u_1} {R : Type u_2} [CommSemiring R] (n : σ →₀ ℕ) (hnn : n ≠ 0) (a : R) : ↑(MvPowerSeries.trunc R n) (↑(MvPowerSeries.C σ R) a) = ↑MvPolynomial.C a

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

noncomputable def MvPowerSeries.inv.aux {σ : Type u_1} {R : Type u_2} [Ring R] (a : R) (φ : MvPowerSeries σ R) : MvPowerSeries σ R

Auxiliary definition that unifies the totalised inverse formal power series (_)⁻¹ and the inverse formal power series that depends on an inverse of the constant coefficient invOfUnit.

Equations

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

theorem MvPowerSeries.coeff_inv_aux {σ : Type u_1} {R : Type u_2} [Ring R] [DecidableEq σ] (n : σ →₀ ℕ) (a : R) (φ : MvPowerSeries σ R) : ↑(MvPowerSeries.coeff R n) (MvPowerSeries.inv.aux a φ) = if n = 0 then a else -a * Finset.sum (Finsupp.antidiagonal n) fun x => if x.snd < n then ↑(MvPowerSeries.coeff R x.fst) φ * ↑(MvPowerSeries.coeff R x.snd) (MvPowerSeries.inv.aux a φ) else 0

def MvPowerSeries.invOfUnit {σ : Type u_1} {R : Type u_2} [Ring R] (φ : MvPowerSeries σ R) (u : Rˣ) : MvPowerSeries σ R

A multivariate formal power series is invertible if the constant coefficient is invertible.

theorem MvPowerSeries.coeff_invOfUnit {σ : Type u_1} {R : Type u_2} [Ring R] [DecidableEq σ] (n : σ →₀ ℕ) (φ : MvPowerSeries σ R) (u : Rˣ) : ↑(MvPowerSeries.coeff R n) (MvPowerSeries.invOfUnit φ u) = if n = 0 then ↑u⁻¹ else -↑u⁻¹ * Finset.sum (Finsupp.antidiagonal n) fun x => if x.snd < n then ↑(MvPowerSeries.coeff R x.fst) φ * ↑(MvPowerSeries.coeff R x.snd) (MvPowerSeries.invOfUnit φ u) else 0

@[simp]

theorem MvPowerSeries.constantCoeff_invOfUnit {σ : Type u_1} {R : Type u_2} [Ring R] (φ : MvPowerSeries σ R) (u : Rˣ) : ↑(MvPowerSeries.constantCoeff σ R) (MvPowerSeries.invOfUnit φ u) = ↑u⁻¹

theorem MvPowerSeries.mul_invOfUnit {σ : Type u_1} {R : Type u_2} [Ring R] (φ : MvPowerSeries σ R) (u : Rˣ) (h : ↑(MvPowerSeries.constantCoeff σ R) φ = ↑u) : φ * MvPowerSeries.invOfUnit φ u = 1

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

Multivariate formal power series over a local ring form a local ring.

instance MvPowerSeries.map.isLocalRingHom {σ : Type u_1} {R : Type u_2} {S : Type u_3} [CommRing R] [CommRing S] (f : R →+* S) [IsLocalRingHom f] : IsLocalRingHom (MvPowerSeries.map σ f)

The map A[[X]] → B[[X]] induced by a local ring hom A → B is local

def MvPowerSeries.inv {σ : Type u_1} {k : Type u_3} [Field k] (φ : MvPowerSeries σ k) : MvPowerSeries σ k

The inverse 1/f of a multivariable power series f over a field

instance MvPowerSeries.instInvMvPowerSeries {σ : Type u_1} {k : Type u_3} [Field k] : Inv (MvPowerSeries σ k)

theorem MvPowerSeries.coeff_inv {σ : Type u_1} {k : Type u_3} [Field k] [DecidableEq σ] (n : σ →₀ ℕ) (φ : MvPowerSeries σ k) : ↑(MvPowerSeries.coeff k n) φ⁻¹ = if n = 0 then (↑(MvPowerSeries.constantCoeff σ k) φ)⁻¹ else -(↑(MvPowerSeries.constantCoeff σ k) φ)⁻¹ * Finset.sum (Finsupp.antidiagonal n) fun x => if x.snd < n then ↑(MvPowerSeries.coeff k x.fst) φ * ↑(MvPowerSeries.coeff k x.snd) φ⁻¹ else 0

@[simp]

theorem MvPowerSeries.constantCoeff_inv {σ : Type u_1} {k : Type u_3} [Field k] (φ : MvPowerSeries σ k) : ↑(MvPowerSeries.constantCoeff σ k) φ⁻¹ = (↑(MvPowerSeries.constantCoeff σ k) φ)⁻¹

theorem MvPowerSeries.inv_eq_zero {σ : Type u_1} {k : Type u_3} [Field k] {φ : MvPowerSeries σ k} : φ⁻¹ = 0 ↔ ↑(MvPowerSeries.constantCoeff σ k) φ = 0

@[simp]

theorem MvPowerSeries.zero_inv {σ : Type u_1} {k : Type u_3} [Field k] : 0⁻¹ = 0

theorem MvPowerSeries.invOfUnit_eq {σ : Type u_1} {k : Type u_3} [Field k] (φ : MvPowerSeries σ k) (h : ↑(MvPowerSeries.constantCoeff σ k) φ ≠ 0) : MvPowerSeries.invOfUnit φ (Units.mk0 (↑(MvPowerSeries.constantCoeff σ k) φ) h) = φ⁻¹

@[simp]

theorem MvPowerSeries.invOfUnit_eq' {σ : Type u_1} {k : Type u_3} [Field k] (φ : MvPowerSeries σ k) (u : kˣ) (h : ↑(MvPowerSeries.constantCoeff σ k) φ = ↑u) : MvPowerSeries.invOfUnit φ u = φ⁻¹

@[simp]

theorem MvPowerSeries.mul_inv_cancel {σ : Type u_1} {k : Type u_3} [Field k] (φ : MvPowerSeries σ k) (h : ↑(MvPowerSeries.constantCoeff σ k) φ ≠ 0) : φ * φ⁻¹ = 1

@[simp]

theorem MvPowerSeries.inv_mul_cancel {σ : Type u_1} {k : Type u_3} [Field k] (φ : MvPowerSeries σ k) (h : ↑(MvPowerSeries.constantCoeff σ k) φ ≠ 0) : φ⁻¹ * φ = 1

theorem MvPowerSeries.eq_mul_inv_iff_mul_eq {σ : Type u_1} {k : Type u_3} [Field k] {φ₁ : MvPowerSeries σ k} {φ₂ : MvPowerSeries σ k} {φ₃ : MvPowerSeries σ k} (h : ↑(MvPowerSeries.constantCoeff σ k) φ₃ ≠ 0) : φ₁ = φ₂ * φ₃⁻¹ ↔ φ₁ * φ₃ = φ₂

theorem MvPowerSeries.eq_inv_iff_mul_eq_one {σ : Type u_1} {k : Type u_3} [Field k] {φ : MvPowerSeries σ k} {ψ : MvPowerSeries σ k} (h : ↑(MvPowerSeries.constantCoeff σ k) ψ ≠ 0) : φ = ψ⁻¹ ↔ φ * ψ = 1

theorem MvPowerSeries.inv_eq_iff_mul_eq_one {σ : Type u_1} {k : Type u_3} [Field k] {φ : MvPowerSeries σ k} {ψ : MvPowerSeries σ k} (h : ↑(MvPowerSeries.constantCoeff σ k) ψ ≠ 0) : ψ⁻¹ = φ ↔ φ * ψ = 1

@[simp]

theorem MvPowerSeries.mul_inv_rev {σ : Type u_1} {k : Type u_3} [Field k] (φ : MvPowerSeries σ k) (ψ : MvPowerSeries σ k) : (φ * ψ)⁻¹ = ψ⁻¹ * φ⁻¹

instance MvPowerSeries.instInvOneClassMvPowerSeries {σ : Type u_1} {k : Type u_3} [Field k] : InvOneClass (MvPowerSeries σ k)

@[simp]

theorem MvPowerSeries.C_inv {σ : Type u_1} {k : Type u_3} [Field k] (r : k) : (↑(MvPowerSeries.C σ k) r)⁻¹ = ↑(MvPowerSeries.C σ k) r⁻¹

@[simp]

theorem MvPowerSeries.X_inv {σ : Type u_1} {k : Type u_3} [Field k] (s : σ) : (MvPowerSeries.X s)⁻¹ = 0

@[simp]

theorem MvPowerSeries.smul_inv {σ : Type u_1} {k : Type u_3} [Field k] (r : k) (φ : MvPowerSeries σ k) : (r • φ)⁻¹ = r⁻¹ • φ⁻¹

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.

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.

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 multivariable polynomials to multivariable power series as a ring homomorphism.

@[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 multivariable polynomials to multivariable power series as an algebra homomorphism.

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

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)

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

def PowerSeries (R : Type u_1) : Type u_1

Formal power series over the coefficient ring R.

instance PowerSeries.instInhabitedPowerSeries {R : Type u_1} [Inhabited R] : Inhabited (PowerSeries R)

instance PowerSeries.instZeroPowerSeries {R : Type u_1} [Zero R] : Zero (PowerSeries R)

instance PowerSeries.instAddMonoidPowerSeries {R : Type u_1} [AddMonoid R] : AddMonoid (PowerSeries R)

instance PowerSeries.instAddGroupPowerSeries {R : Type u_1} [AddGroup R] : AddGroup (PowerSeries R)

instance PowerSeries.instAddCommMonoidPowerSeries {R : Type u_1} [AddCommMonoid R] : AddCommMonoid (PowerSeries R)

instance PowerSeries.instAddCommGroupPowerSeries {R : Type u_1} [AddCommGroup R] : AddCommGroup (PowerSeries R)

instance PowerSeries.instSemiringPowerSeries {R : Type u_1} [Semiring R] : Semiring (PowerSeries R)

instance PowerSeries.instCommSemiringPowerSeries {R : Type u_1} [CommSemiring R] : CommSemiring (PowerSeries R)

instance PowerSeries.instRingPowerSeries {R : Type u_1} [Ring R] : Ring (PowerSeries R)

instance PowerSeries.instCommRingPowerSeries {R : Type u_1} [CommRing R] : CommRing (PowerSeries R)

instance PowerSeries.instNontrivialPowerSeries {R : Type u_1} [Nontrivial R] : Nontrivial (PowerSeries R)

instance PowerSeries.instModulePowerSeriesInstAddCommMonoidPowerSeries {R : Type u_1} {A : Type u_2} [Semiring R] [AddCommMonoid A] [Module R A] : Module R (PowerSeries A)

instance PowerSeries.instIsScalarTowerPowerSeriesToSMulInstZeroPowerSeriesToZeroToAddMonoidToSMulZeroClassToZeroToMonoidWithZeroToSMulWithZeroToMulActionWithZeroInstAddCommMonoidPowerSeriesInstModulePowerSeriesInstAddCommMonoidPowerSeriesToSMulToSMulZeroClassToZeroToMonoidWithZeroToSMulWithZeroToMulActionWithZeroInstModulePowerSeriesInstAddCommMonoidPowerSeries {R : Type u_1} {A : Type u_2} {S : Type u_3} [Semiring R] [Semiring S] [AddCommMonoid A] [Module R A] [Module S A] [SMul R S] [IsScalarTower R S A] : IsScalarTower R S (PowerSeries A)

instance PowerSeries.instAlgebraPowerSeriesInstSemiringPowerSeries {R : Type u_1} {A : Type u_2} [Semiring A] [CommSemiring R] [Algebra R A] : Algebra R (PowerSeries A)

def PowerSeries.coeff (R : Type u_1) [Semiring R] (n : ℕ) : PowerSeries R →ₗ[R] R

The nth coefficient of a formal power series.

def PowerSeries.monomial (R : Type u_1) [Semiring R] (n : ℕ) : R →ₗ[R] PowerSeries R

The nth monomial with coefficient a as formal power series.

theorem PowerSeries.coeff_def {R : Type u_1} [Semiring R] {s : Unit →₀ ℕ} {n : ℕ} (h : ↑s () = n) : PowerSeries.coeff R n = MvPowerSeries.coeff R s

theorem PowerSeries.ext {R : Type u_1} [Semiring R] {φ : PowerSeries R} {ψ : PowerSeries R} (h : ∀ (n : ℕ), ↑(PowerSeries.coeff R n) φ = ↑(PowerSeries.coeff R n) ψ) : φ = ψ

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

theorem PowerSeries.ext_iff {R : Type u_1} [Semiring R] {φ : PowerSeries R} {ψ : PowerSeries R} : φ = ψ ↔ ∀ (n : ℕ), ↑(PowerSeries.coeff R n) φ = ↑(PowerSeries.coeff R n) ψ

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

def PowerSeries.mk {R : Type u_2} (f : ℕ → R) : PowerSeries R

Constructor for formal power series.

@[simp]

theorem PowerSeries.coeff_mk {R : Type u_1} [Semiring R] (n : ℕ) (f : ℕ → R) : ↑(PowerSeries.coeff R n) (PowerSeries.mk f) = f n

theorem PowerSeries.coeff_monomial {R : Type u_1} [Semiring R] (m : ℕ) (n : ℕ) (a : R) : ↑(PowerSeries.coeff R m) (↑(PowerSeries.monomial R n) a) = if m = n then a else 0

theorem PowerSeries.monomial_eq_mk {R : Type u_1} [Semiring R] (n : ℕ) (a : R) : ↑(PowerSeries.monomial R n) a = PowerSeries.mk fun m => if m = n then a else 0

@[simp]

theorem PowerSeries.coeff_monomial_same {R : Type u_1} [Semiring R] (n : ℕ) (a : R) : ↑(PowerSeries.coeff R n) (↑(PowerSeries.monomial R n) a) = a

@[simp]

theorem PowerSeries.coeff_comp_monomial {R : Type u_1} [Semiring R] (n : ℕ) : LinearMap.comp (PowerSeries.coeff R n) (PowerSeries.monomial R n) = LinearMap.id

def PowerSeries.constantCoeff (R : Type u_1) [Semiring R] : PowerSeries R →+* R

The constant coefficient of a formal power series.

def PowerSeries.C (R : Type u_1) [Semiring R] : R →+* PowerSeries R

The constant formal power series.

def PowerSeries.X {R : Type u_1} [Semiring R] : PowerSeries R

The variable of the formal power series ring.

theorem PowerSeries.commute_X {R : Type u_1} [Semiring R] (φ : PowerSeries R) : Commute φ PowerSeries.X

@[simp]

theorem PowerSeries.coeff_zero_eq_constantCoeff {R : Type u_1} [Semiring R] : ↑(PowerSeries.coeff R 0) = ↑(PowerSeries.constantCoeff R)

theorem PowerSeries.coeff_zero_eq_constantCoeff_apply {R : Type u_1} [Semiring R] (φ : PowerSeries R) : ↑(PowerSeries.coeff R 0) φ = ↑(PowerSeries.constantCoeff R) φ

@[simp]

theorem PowerSeries.monomial_zero_eq_C {R : Type u_1} [Semiring R] : ↑(PowerSeries.monomial R 0) = ↑(PowerSeries.C R)

theorem PowerSeries.monomial_zero_eq_C_apply {R : Type u_1} [Semiring R] (a : R) : ↑(PowerSeries.monomial R 0) a = ↑(PowerSeries.C R) a

theorem PowerSeries.coeff_C {R : Type u_1} [Semiring R] (n : ℕ) (a : R) : ↑(PowerSeries.coeff R n) (↑(PowerSeries.C R) a) = if n = 0 then a else 0

@[simp]

theorem PowerSeries.coeff_zero_C {R : Type u_1} [Semiring R] (a : R) : ↑(PowerSeries.coeff R 0) (↑(PowerSeries.C R) a) = a

theorem PowerSeries.X_eq {R : Type u_1} [Semiring R] : PowerSeries.X = ↑(PowerSeries.monomial R 1) 1

theorem PowerSeries.coeff_X {R : Type u_1} [Semiring R] (n : ℕ) : ↑(PowerSeries.coeff R n) PowerSeries.X = if n = 1 then 1 else 0

@[simp]

theorem PowerSeries.coeff_zero_X {R : Type u_1} [Semiring R] : ↑(PowerSeries.coeff R 0) PowerSeries.X = 0

@[simp]

theorem PowerSeries.coeff_one_X {R : Type u_1} [Semiring R] : ↑(PowerSeries.coeff R 1) PowerSeries.X = 1

@[simp]

theorem PowerSeries.X_ne_zero {R : Type u_1} [Semiring R] [Nontrivial R] : PowerSeries.X ≠ 0

theorem PowerSeries.X_pow_eq {R : Type u_1} [Semiring R] (n : ℕ) : PowerSeries.X ^ n = ↑(PowerSeries.monomial R n) 1

theorem PowerSeries.coeff_X_pow {R : Type u_1} [Semiring R] (m : ℕ) (n : ℕ) : ↑(PowerSeries.coeff R m) (PowerSeries.X ^ n) = if m = n then 1 else 0

@[simp]

theorem PowerSeries.coeff_X_pow_self {R : Type u_1} [Semiring R] (n : ℕ) : ↑(PowerSeries.coeff R n) (PowerSeries.X ^ n) = 1

@[simp]

theorem PowerSeries.coeff_one {R : Type u_1} [Semiring R] (n : ℕ) : ↑(PowerSeries.coeff R n) 1 = if n = 0 then 1 else 0

theorem PowerSeries.coeff_zero_one {R : Type u_1} [Semiring R] : ↑(PowerSeries.coeff R 0) 1 = 1

theorem PowerSeries.coeff_mul {R : Type u_1} [Semiring R] (n : ℕ) (φ : PowerSeries R) (ψ : PowerSeries R) : ↑(PowerSeries.coeff R n) (φ * ψ) = Finset.sum (Finset.Nat.antidiagonal n) fun p => ↑(PowerSeries.coeff R p.fst) φ * ↑(PowerSeries.coeff R p.snd) ψ

@[simp]

theorem PowerSeries.coeff_mul_C {R : Type u_1} [Semiring R] (n : ℕ) (φ : PowerSeries R) (a : R) : ↑(PowerSeries.coeff R n) (φ * ↑(PowerSeries.C R) a) = ↑(PowerSeries.coeff R n) φ * a

@[simp]

theorem PowerSeries.coeff_C_mul {R : Type u_1} [Semiring R] (n : ℕ) (φ : PowerSeries R) (a : R) : ↑(PowerSeries.coeff R n) (↑(PowerSeries.C R) a * φ) = a * ↑(PowerSeries.coeff R n) φ

@[simp]

theorem PowerSeries.coeff_smul {R : Type u_1} [Semiring R] {S : Type u_2} [Semiring S] [Module R S] (n : ℕ) (φ : PowerSeries S) (a : R) : ↑(PowerSeries.coeff S n) (a • φ) = a • ↑(PowerSeries.coeff S n) φ

theorem PowerSeries.smul_eq_C_mul {R : Type u_1} [Semiring R] (f : PowerSeries R) (a : R) : a • f = ↑(PowerSeries.C R) a * f

@[simp]

theorem PowerSeries.coeff_succ_mul_X {R : Type u_1} [Semiring R] (n : ℕ) (φ : PowerSeries R) : ↑(PowerSeries.coeff R (n + 1)) (φ * PowerSeries.X) = ↑(PowerSeries.coeff R n) φ

@[simp]

theorem PowerSeries.coeff_succ_X_mul {R : Type u_1} [Semiring R] (n : ℕ) (φ : PowerSeries R) : ↑(PowerSeries.coeff R (n + 1)) (PowerSeries.X * φ) = ↑(PowerSeries.coeff R n) φ

@[simp]

theorem PowerSeries.constantCoeff_C {R : Type u_1} [Semiring R] (a : R) : ↑(PowerSeries.constantCoeff R) (↑(PowerSeries.C R) a) = a

@[simp]

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

theorem PowerSeries.constantCoeff_zero {R : Type u_1} [Semiring R] : ↑(PowerSeries.constantCoeff R) 0 = 0

theorem PowerSeries.constantCoeff_one {R : Type u_1} [Semiring R] : ↑(PowerSeries.constantCoeff R) 1 = 1

@[simp]

theorem PowerSeries.constantCoeff_X {R : Type u_1} [Semiring R] : ↑(PowerSeries.constantCoeff R) PowerSeries.X = 0

theorem PowerSeries.coeff_zero_mul_X {R : Type u_1} [Semiring R] (φ : PowerSeries R) : ↑(PowerSeries.coeff R 0) (φ * PowerSeries.X) = 0

theorem PowerSeries.coeff_zero_X_mul {R : Type u_1} [Semiring R] (φ : PowerSeries R) : ↑(PowerSeries.coeff R 0) (PowerSeries.X * φ) = 0

theorem PowerSeries.coeff_C_mul_X_pow {R : Type u_1} [Semiring R] (x : R) (k : ℕ) (n : ℕ) : ↑(PowerSeries.coeff R n) (↑(PowerSeries.C R) x * PowerSeries.X ^ k) = if n = k then x else 0

@[simp]

theorem PowerSeries.coeff_mul_X_pow {R : Type u_1} [Semiring R] (p : PowerSeries R) (n : ℕ) (d : ℕ) : ↑(PowerSeries.coeff R (d + n)) (p * PowerSeries.X ^ n) = ↑(PowerSeries.coeff R d) p

@[simp]

theorem PowerSeries.coeff_X_pow_mul {R : Type u_1} [Semiring R] (p : PowerSeries R) (n : ℕ) (d : ℕ) : ↑(PowerSeries.coeff R (d + n)) (PowerSeries.X ^ n * p) = ↑(PowerSeries.coeff R d) p

theorem PowerSeries.coeff_mul_X_pow' {R : Type u_1} [Semiring R] (p : PowerSeries R) (n : ℕ) (d : ℕ) : ↑(PowerSeries.coeff R d) (p * PowerSeries.X ^ n) = if n ≤ d then ↑(PowerSeries.coeff R (d - n)) p else 0

theorem PowerSeries.coeff_X_pow_mul' {R : Type u_1} [Semiring R] (p : PowerSeries R) (n : ℕ) (d : ℕ) : ↑(PowerSeries.coeff R d) (PowerSeries.X ^ n * p) = if n ≤ d then ↑(PowerSeries.coeff R (d - n)) p else 0

theorem PowerSeries.isUnit_constantCoeff {R : Type u_1} [Semiring R] (φ : PowerSeries R) (h : IsUnit φ) : IsUnit (↑(PowerSeries.constantCoeff R) φ)

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

theorem PowerSeries.eq_shift_mul_X_add_const {R : Type u_1} [Semiring R] (φ : PowerSeries R) : φ = (PowerSeries.mk fun p => ↑(PowerSeries.coeff R (p + 1)) φ) * PowerSeries.X + ↑(PowerSeries.C R) (↑(PowerSeries.constantCoeff R) φ)

Split off the constant coefficient.

theorem PowerSeries.eq_X_mul_shift_add_const {R : Type u_1} [Semiring R] (φ : PowerSeries R) : φ = (PowerSeries.X * PowerSeries.mk fun p => ↑(PowerSeries.coeff R (p + 1)) φ) + ↑(PowerSeries.C R) (↑(PowerSeries.constantCoeff R) φ)

Split off the constant coefficient.

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

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

@[simp]

theorem PowerSeries.map_id {R : Type u_1} [Semiring R] : ↑(PowerSeries.map (RingHom.id R)) = id

theorem PowerSeries.map_comp {R : Type u_1} [Semiring R] {S : Type u_2} {T : Type u_3} [Semiring S] [Semiring T] (f : R →+* S) (g : S →+* T) : PowerSeries.map (RingHom.comp g f) = RingHom.comp (PowerSeries.map g) (PowerSeries.map f)

@[simp]

theorem PowerSeries.coeff_map {R : Type u_1} [Semiring R] {S : Type u_2} [Semiring S] (f : R →+* S) (n : ℕ) (φ : PowerSeries R) : ↑(PowerSeries.coeff S n) (↑(PowerSeries.map f) φ) = ↑f (↑(PowerSeries.coeff R n) φ)

@[simp]

theorem PowerSeries.map_C {R : Type u_1} [Semiring R] {S : Type u_2} [Semiring S] (f : R →+* S) (r : R) : ↑(PowerSeries.map f) (↑(PowerSeries.C R) r) = ↑(PowerSeries.C ((fun x => S) r)) (↑f r)

@[simp]

theorem PowerSeries.map_X {R : Type u_1} [Semiring R] {S : Type u_2} [Semiring S] (f : R →+* S) : ↑(PowerSeries.map f) PowerSeries.X = PowerSeries.X

theorem PowerSeries.X_pow_dvd_iff {R : Type u_1} [Semiring R] {n : ℕ} {φ : PowerSeries R} : PowerSeries.X ^ n ∣ φ ↔ ∀ (m : ℕ), m < n → ↑(PowerSeries.coeff R m) φ = 0

theorem PowerSeries.X_dvd_iff {R : Type u_1} [Semiring R] {φ : PowerSeries R} : PowerSeries.X ∣ φ ↔ ↑(PowerSeries.constantCoeff R) φ = 0

noncomputable def PowerSeries.rescale {R : Type u_1} [CommSemiring R] (a : R) : PowerSeries R →+* PowerSeries R

The ring homomorphism taking a power series f(X) to f(aX).

@[simp]

theorem PowerSeries.coeff_rescale {R : Type u_1} [CommSemiring R] (f : PowerSeries R) (a : R) (n : ℕ) : ↑(PowerSeries.coeff R n) (↑(PowerSeries.rescale a) f) = a ^ n * ↑(PowerSeries.coeff R n) f

@[simp]

theorem PowerSeries.rescale_zero {R : Type u_1} [CommSemiring R] : PowerSeries.rescale 0 = RingHom.comp (PowerSeries.C R) (PowerSeries.constantCoeff R)

theorem PowerSeries.rescale_zero_apply {R : Type u_1} [CommSemiring R] : ↑(PowerSeries.rescale 0) PowerSeries.X = ↑(PowerSeries.C R) (↑(PowerSeries.constantCoeff R) PowerSeries.X)

@[simp]

theorem PowerSeries.rescale_one {R : Type u_1} [CommSemiring R] : PowerSeries.rescale 1 = RingHom.id (PowerSeries R)

theorem PowerSeries.rescale_mk {R : Type u_1} [CommSemiring R] (f : ℕ → R) (a : R) : ↑(PowerSeries.rescale a) (PowerSeries.mk f) = PowerSeries.mk fun n => a ^ n * f n

theorem PowerSeries.rescale_rescale {R : Type u_1} [CommSemiring R] (f : PowerSeries R) (a : R) (b : R) : ↑(PowerSeries.rescale b) (↑(PowerSeries.rescale a) f) = ↑(PowerSeries.rescale (a * b)) f

theorem PowerSeries.rescale_mul {R : Type u_1} [CommSemiring R] (a : R) (b : R) : PowerSeries.rescale (a * b) = RingHom.comp (PowerSeries.rescale b) (PowerSeries.rescale a)

def PowerSeries.trunc {R : Type u_1} [CommSemiring R] (n : ℕ) (φ : PowerSeries R) : Polynomial R

The nth truncation of a formal power series to a polynomial

theorem PowerSeries.coeff_trunc {R : Type u_1} [CommSemiring R] (m : ℕ) (n : ℕ) (φ : PowerSeries R) : Polynomial.coeff (PowerSeries.trunc n φ) m = if m < n then ↑(PowerSeries.coeff R m) φ else 0

@[simp]

theorem PowerSeries.trunc_zero {R : Type u_1} [CommSemiring R] (n : ℕ) : PowerSeries.trunc n 0 = 0

@[simp]

theorem PowerSeries.trunc_one {R : Type u_1} [CommSemiring R] (n : ℕ) : PowerSeries.trunc (n + 1) 1 = 1

@[simp]

theorem PowerSeries.trunc_C {R : Type u_1} [CommSemiring R] (n : ℕ) (a : R) : PowerSeries.trunc (n + 1) (↑(PowerSeries.C R) a) = ↑Polynomial.C a

@[simp]

theorem PowerSeries.trunc_add {R : Type u_1} [CommSemiring R] (n : ℕ) (φ : PowerSeries R) (ψ : PowerSeries R) : PowerSeries.trunc n (φ + ψ) = PowerSeries.trunc n φ + PowerSeries.trunc n ψ

def PowerSeries.inv.aux {R : Type u_1} [Ring R] : R → PowerSeries R → PowerSeries R

Auxiliary function used for computing inverse of a power series

theorem PowerSeries.coeff_inv_aux {R : Type u_1} [Ring R] (n : ℕ) (a : R) (φ : PowerSeries R) : ↑(PowerSeries.coeff R n) (PowerSeries.inv.aux a φ) = if n = 0 then a else -a * Finset.sum (Finset.Nat.antidiagonal n) fun x => if x.snd < n then ↑(PowerSeries.coeff R x.fst) φ * ↑(PowerSeries.coeff R x.snd) (PowerSeries.inv.aux a φ) else 0

def PowerSeries.invOfUnit {R : Type u_1} [Ring R] (φ : PowerSeries R) (u : Rˣ) : PowerSeries R

A formal power series is invertible if the constant coefficient is invertible.

theorem PowerSeries.coeff_invOfUnit {R : Type u_1} [Ring R] (n : ℕ) (φ : PowerSeries R) (u : Rˣ) : ↑(PowerSeries.coeff R n) (PowerSeries.invOfUnit φ u) = if n = 0 then ↑u⁻¹ else -↑u⁻¹ * Finset.sum (Finset.Nat.antidiagonal n) fun x => if x.snd < n then ↑(PowerSeries.coeff R x.fst) φ * ↑(PowerSeries.coeff R x.snd) (PowerSeries.invOfUnit φ u) else 0

@[simp]

theorem PowerSeries.constantCoeff_invOfUnit {R : Type u_1} [Ring R] (φ : PowerSeries R) (u : Rˣ) : ↑(PowerSeries.constantCoeff R) (PowerSeries.invOfUnit φ u) = ↑u⁻¹

theorem PowerSeries.mul_invOfUnit {R : Type u_1} [Ring R] (φ : PowerSeries R) (u : Rˣ) (h : ↑(PowerSeries.constantCoeff R) φ = ↑u) : φ * PowerSeries.invOfUnit φ u = 1

theorem PowerSeries.sub_const_eq_shift_mul_X {R : Type u_1} [Ring R] (φ : PowerSeries R) : φ - ↑(PowerSeries.C R) (↑(PowerSeries.constantCoeff R) φ) = (PowerSeries.mk fun p => ↑(PowerSeries.coeff R (p + 1)) φ) * PowerSeries.X

Two ways of removing the constant coefficient of a power series are the same.

theorem PowerSeries.sub_const_eq_X_mul_shift {R : Type u_1} [Ring R] (φ : PowerSeries R) : φ - ↑(PowerSeries.C R) (↑(PowerSeries.constantCoeff R) φ) = PowerSeries.X * PowerSeries.mk fun p => ↑(PowerSeries.coeff R (p + 1)) φ

@[simp]

theorem PowerSeries.rescale_X {A : Type u_2} [CommRing A] (a : A) : ↑(PowerSeries.rescale a) PowerSeries.X = ↑(PowerSeries.C A) a * PowerSeries.X

theorem PowerSeries.rescale_neg_one_X {A : Type u_2} [CommRing A] : ↑(PowerSeries.rescale (-1)) PowerSeries.X = -PowerSeries.X

noncomputable def PowerSeries.evalNegHom {A : Type u_2} [CommRing A] : PowerSeries A →+* PowerSeries A

The ring homomorphism taking a power series f(X) to f(-X).

@[simp]

theorem PowerSeries.evalNegHom_X {A : Type u_2} [CommRing A] : ↑PowerSeries.evalNegHom PowerSeries.X = -PowerSeries.X

theorem PowerSeries.eq_zero_or_eq_zero_of_mul_eq_zero {R : Type u_1} [Ring R] [NoZeroDivisors R] (φ : PowerSeries R) (ψ : PowerSeries R) (h : φ * ψ = 0) : φ = 0 ∨ ψ = 0

instance PowerSeries.instNoZeroDivisorsPowerSeriesToMulToNonUnitalNonAssocRingToNonAssocRingInstRingPowerSeriesInstZeroPowerSeriesToZeroToMonoidWithZeroToSemiring {R : Type u_1} [Ring R] [NoZeroDivisors R] : NoZeroDivisors (PowerSeries R)

instance PowerSeries.instIsDomainPowerSeriesInstSemiringPowerSeriesToSemiring {R : Type u_1} [Ring R] [IsDomain R] : IsDomain (PowerSeries R)

theorem PowerSeries.span_X_isPrime {R : Type u_1} [CommRing R] [IsDomain R] : Ideal.IsPrime (Ideal.span {PowerSeries.X})

The ideal spanned by the variable in the power series ring over an integral domain is a prime ideal.

theorem PowerSeries.X_prime {R : Type u_1} [CommRing R] [IsDomain R] : Prime PowerSeries.X

The variable of the power series ring over an integral domain is prime.

theorem PowerSeries.rescale_injective {R : Type u_1} [CommRing R] [IsDomain R] {a : R} (ha : a ≠ 0) : Function.Injective ↑(PowerSeries.rescale a)

instance PowerSeries.map.isLocalRingHom {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] (f : R →+* S) [IsLocalRingHom f] : IsLocalRingHom (PowerSeries.map f)

instance PowerSeries.instLocalRingPowerSeriesInstSemiringPowerSeriesToSemiringToCommSemiring {R : Type u_1} [CommRing R] [LocalRing R] : LocalRing (PowerSeries R)

theorem PowerSeries.C_eq_algebraMap {R : Type u_1} [CommSemiring R] {r : R} : ↑(PowerSeries.C R) r = ↑(algebraMap R (PowerSeries R)) r

theorem PowerSeries.algebraMap_apply {R : Type u_1} {A : Type u_2} [CommSemiring R] [Semiring A] [Algebra R A] {r : R} : ↑(algebraMap R (PowerSeries A)) r = ↑(PowerSeries.C A) (↑(algebraMap R A) r)

instance PowerSeries.instNontrivialSubalgebraPowerSeriesInstSemiringPowerSeriesToSemiringInstAlgebraPowerSeriesInstSemiringPowerSeriesId {R : Type u_1} [CommSemiring R] [Nontrivial R] : Nontrivial (Subalgebra R (PowerSeries R))

def PowerSeries.inv {k : Type u_2} [Field k] : PowerSeries k → PowerSeries k

The inverse 1/f of a power series f defined over a field

instance PowerSeries.instInvPowerSeries {k : Type u_2} [Field k] : Inv (PowerSeries k)

theorem PowerSeries.inv_eq_inv_aux {k : Type u_2} [Field k] (φ : PowerSeries k) : φ⁻¹ = PowerSeries.inv.aux (↑(PowerSeries.constantCoeff k) φ)⁻¹ φ

theorem PowerSeries.coeff_inv {k : Type u_2} [Field k] (n : ℕ) (φ : PowerSeries k) : ↑(PowerSeries.coeff k n) φ⁻¹ = if n = 0 then (↑(PowerSeries.constantCoeff k) φ)⁻¹ else -(↑(PowerSeries.constantCoeff k) φ)⁻¹ * Finset.sum (Finset.Nat.antidiagonal n) fun x => if x.snd < n then ↑(PowerSeries.coeff k x.fst) φ * ↑(PowerSeries.coeff k x.snd) φ⁻¹ else 0

@[simp]

theorem PowerSeries.constantCoeff_inv {k : Type u_2} [Field k] (φ : PowerSeries k) : ↑(PowerSeries.constantCoeff k) φ⁻¹ = (↑(PowerSeries.constantCoeff k) φ)⁻¹

theorem PowerSeries.inv_eq_zero {k : Type u_2} [Field k] {φ : PowerSeries k} : φ⁻¹ = 0 ↔ ↑(PowerSeries.constantCoeff k) φ = 0

@[simp]

theorem PowerSeries.zero_inv {k : Type u_2} [Field k] : 0⁻¹ = 0

theorem PowerSeries.invOfUnit_eq {k : Type u_2} [Field k] (φ : PowerSeries k) (h : ↑(PowerSeries.constantCoeff k) φ ≠ 0) : PowerSeries.invOfUnit φ (Units.mk0 (↑(PowerSeries.constantCoeff k) φ) h) = φ⁻¹

@[simp]

theorem PowerSeries.invOfUnit_eq' {k : Type u_2} [Field k] (φ : PowerSeries k) (u : kˣ) (h : ↑(PowerSeries.constantCoeff k) φ = ↑u) : PowerSeries.invOfUnit φ u = φ⁻¹

@[simp]

theorem PowerSeries.mul_inv_cancel {k : Type u_2} [Field k] (φ : PowerSeries k) (h : ↑(PowerSeries.constantCoeff k) φ ≠ 0) : φ * φ⁻¹ = 1

@[simp]

theorem PowerSeries.inv_mul_cancel {k : Type u_2} [Field k] (φ : PowerSeries k) (h : ↑(PowerSeries.constantCoeff k) φ ≠ 0) : φ⁻¹ * φ = 1

theorem PowerSeries.eq_mul_inv_iff_mul_eq {k : Type u_2} [Field k] {φ₁ : PowerSeries k} {φ₂ : PowerSeries k} {φ₃ : PowerSeries k} (h : ↑(PowerSeries.constantCoeff k) φ₃ ≠ 0) : φ₁ = φ₂ * φ₃⁻¹ ↔ φ₁ * φ₃ = φ₂

theorem PowerSeries.eq_inv_iff_mul_eq_one {k : Type u_2} [Field k] {φ : PowerSeries k} {ψ : PowerSeries k} (h : ↑(PowerSeries.constantCoeff k) ψ ≠ 0) : φ = ψ⁻¹ ↔ φ * ψ = 1

theorem PowerSeries.inv_eq_iff_mul_eq_one {k : Type u_2} [Field k] {φ : PowerSeries k} {ψ : PowerSeries k} (h : ↑(PowerSeries.constantCoeff k) ψ ≠ 0) : ψ⁻¹ = φ ↔ φ * ψ = 1

@[simp]

theorem PowerSeries.mul_inv_rev {k : Type u_2} [Field k] (φ : PowerSeries k) (ψ : PowerSeries k) : (φ * ψ)⁻¹ = ψ⁻¹ * φ⁻¹

instance PowerSeries.instInvOneClassPowerSeries {k : Type u_2} [Field k] : InvOneClass (PowerSeries k)

@[simp]

theorem PowerSeries.C_inv {k : Type u_2} [Field k] (r : k) : (↑(PowerSeries.C k) r)⁻¹ = ↑(PowerSeries.C k) r⁻¹

@[simp]

theorem PowerSeries.X_inv {k : Type u_2} [Field k] : PowerSeries.X⁻¹ = 0

@[simp]

theorem PowerSeries.smul_inv {k : Type u_2} [Field k] (r : k) (φ : PowerSeries k) : (r • φ)⁻¹ = r⁻¹ • φ⁻¹

theorem PowerSeries.exists_coeff_ne_zero_iff_ne_zero {R : Type u_1} [Semiring R] {φ : PowerSeries R} : (∃ n, ↑(PowerSeries.coeff R n) φ ≠ 0) ↔ φ ≠ 0

def PowerSeries.order {R : Type u_1} [Semiring R] (φ : PowerSeries R) : PartENat

The order of a formal power series φ is the greatest n : PartENat such that X^n divides φ. The order is ⊤ if and only if φ = 0.

@[simp]

theorem PowerSeries.order_zero {R : Type u_1} [Semiring R] : PowerSeries.order 0 = ⊤

The order of the 0 power series is infinite.

theorem PowerSeries.order_finite_iff_ne_zero {R : Type u_1} [Semiring R] {φ : PowerSeries R} : (PowerSeries.order φ).Dom ↔ φ ≠ 0

theorem PowerSeries.coeff_order {R : Type u_1} [Semiring R] {φ : PowerSeries R} (h : (PowerSeries.order φ).Dom) : ↑(PowerSeries.coeff R (Part.get (PowerSeries.order φ) h)) φ ≠ 0

If the order of a formal power series is finite, then the coefficient indexed by the order is nonzero.

theorem PowerSeries.order_le {R : Type u_1} [Semiring R] {φ : PowerSeries R} (n : ℕ) (h : ↑(PowerSeries.coeff R n) φ ≠ 0) : PowerSeries.order φ ≤ ↑n

If the nth coefficient of a formal power series is nonzero, then the order of the power series is less than or equal to n.

theorem PowerSeries.coeff_of_lt_order {R : Type u_1} [Semiring R] {φ : PowerSeries R} (n : ℕ) (h : ↑n < PowerSeries.order φ) : ↑(PowerSeries.coeff R n) φ = 0

The nth coefficient of a formal power series is 0 if n is strictly smaller than the order of the power series.

@[simp]

theorem PowerSeries.order_eq_top {R : Type u_1} [Semiring R] {φ : PowerSeries R} : PowerSeries.order φ = ⊤ ↔ φ = 0

The 0 power series is the unique power series with infinite order.

theorem PowerSeries.nat_le_order {R : Type u_1} [Semiring R] (φ : PowerSeries R) (n : ℕ) (h : ∀ (i : ℕ), i < n → ↑(PowerSeries.coeff R i) φ = 0) : ↑n ≤ PowerSeries.order φ

The order of a formal power series is at least n if the ith coefficient is 0 for all i < n.

theorem PowerSeries.le_order {R : Type u_1} [Semiring R] (φ : PowerSeries R) (n : PartENat) (h : ∀ (i : ℕ), ↑i < n → ↑(PowerSeries.coeff R i) φ = 0) : n ≤ PowerSeries.order φ

The order of a formal power series is at least n if the ith coefficient is 0 for all i < n.

theorem PowerSeries.order_eq_nat {R : Type u_1} [Semiring R] {φ : PowerSeries R} {n : ℕ} : PowerSeries.order φ = ↑n ↔ ↑(PowerSeries.coeff R n) φ ≠ 0 ∧ ∀ (i : ℕ), i < n → ↑(PowerSeries.coeff R i) φ = 0

The order of a formal power series is exactly n if the nth coefficient is nonzero, and the ith coefficient is 0 for all i < n.

theorem PowerSeries.order_eq {R : Type u_1} [Semiring R] {φ : PowerSeries R} {n : PartENat} : PowerSeries.order φ = n ↔ (∀ (i : ℕ), ↑i = n → ↑(PowerSeries.coeff R i) φ ≠ 0) ∧ ∀ (i : ℕ), ↑i < n → ↑(PowerSeries.coeff R i) φ = 0

The order of a formal power series is exactly n if the nth coefficient is nonzero, and the ith coefficient is 0 for all i < n.

theorem PowerSeries.le_order_add {R : Type u_1} [Semiring R] (φ : PowerSeries R) (ψ : PowerSeries R) : min (PowerSeries.order φ) (PowerSeries.order ψ) ≤ PowerSeries.order (φ + ψ)

The order of the sum of two formal power series is at least the minimum of their orders.

theorem PowerSeries.order_add_of_order_eq {R : Type u_1} [Semiring R] (φ : PowerSeries R) (ψ : PowerSeries R) (h : PowerSeries.order φ ≠ PowerSeries.order ψ) : PowerSeries.order (φ + ψ) = PowerSeries.order φ ⊓ PowerSeries.order ψ

The order of the sum of two formal power series is the minimum of their orders if their orders differ.

theorem PowerSeries.order_mul_ge {R : Type u_1} [Semiring R] (φ : PowerSeries R) (ψ : PowerSeries R) : PowerSeries.order φ + PowerSeries.order ψ ≤ PowerSeries.order (φ * ψ)

The order of the product of two formal power series is at least the sum of their orders.

theorem PowerSeries.order_monomial {R : Type u_1} [Semiring R] (n : ℕ) (a : R) [Decidable (a = 0)] : PowerSeries.order (↑(PowerSeries.monomial R n) a) = if a = 0 then ⊤ else ↑n

The order of the monomial a*X^n is infinite if a = 0 and n otherwise.

theorem PowerSeries.order_monomial_of_ne_zero {R : Type u_1} [Semiring R] (n : ℕ) (a : R) (h : a ≠ 0) : PowerSeries.order (↑(PowerSeries.monomial R n) a) = ↑n

The order of the monomial a*X^n is n if a ≠ 0.

theorem PowerSeries.coeff_mul_of_lt_order {R : Type u_1} [Semiring R] {φ : PowerSeries R} {ψ : PowerSeries R} {n : ℕ} (h : ↑n < PowerSeries.order ψ) : ↑(PowerSeries.coeff R n) (φ * ψ) = 0

If n is strictly smaller than the order of ψ, then the nth coefficient of its product with any other power series is 0.

theorem PowerSeries.coeff_mul_one_sub_of_lt_order {R : Type u_2} [CommRing R] {φ : PowerSeries R} {ψ : PowerSeries R} (n : ℕ) (h : ↑n < PowerSeries.order ψ) : ↑(PowerSeries.coeff R n) (φ * (1 - ψ)) = ↑(PowerSeries.coeff R n) φ

theorem PowerSeries.coeff_mul_prod_one_sub_of_lt_order {R : Type u_2} {ι : Type u_3} [CommRing R] (k : ℕ) (s : Finset ι) (φ : PowerSeries R) (f : ι → PowerSeries R) : (∀ (i : ι), i ∈ s → ↑k < PowerSeries.order (f i)) → ↑(PowerSeries.coeff R k) (φ * Finset.prod s fun i => 1 - f i) = ↑(PowerSeries.coeff R k) φ

theorem PowerSeries.X_pow_order_dvd {R : Type u_1} [Semiring R] {φ : PowerSeries R} (h : (PowerSeries.order φ).Dom) : PowerSeries.X ^ Part.get (PowerSeries.order φ) h ∣ φ

theorem PowerSeries.order_eq_multiplicity_X {R : Type u_2} [Semiring R] (φ : PowerSeries R) : PowerSeries.order φ = multiplicity PowerSeries.X φ

@[simp]

theorem PowerSeries.order_one {R : Type u_1} [Semiring R] [Nontrivial R] : PowerSeries.order 1 = 0

The order of the formal power series 1 is 0.

@[simp]

theorem PowerSeries.order_X {R : Type u_1} [Semiring R] [Nontrivial R] : PowerSeries.order PowerSeries.X = 1

The order of the formal power series X is 1.

@[simp]

theorem PowerSeries.order_X_pow {R : Type u_1} [Semiring R] [Nontrivial R] (n : ℕ) : PowerSeries.order (PowerSeries.X ^ n) = ↑n

The order of the formal power series X^n is n.

theorem PowerSeries.order_mul {R : Type u_1} [CommRing R] [IsDomain R] (φ : PowerSeries R) (ψ : PowerSeries R) : PowerSeries.order (φ * ψ) = PowerSeries.order φ + PowerSeries.order ψ

The order of the product of two formal power series over an integral domain is the sum of their orders.

def Polynomial.ToPowerSeries {R : Type u_2} [CommSemiring R] : Polynomial R → PowerSeries R

The natural inclusion from polynomials into formal power series.

instance Polynomial.coeToPowerSeries {R : Type u_2} [CommSemiring R] : Coe (Polynomial R) (PowerSeries R)

The natural inclusion from polynomials into formal power series.

theorem Polynomial.coe_def {R : Type u_2} [CommSemiring R] (φ : Polynomial R) : ↑φ = PowerSeries.mk (Polynomial.coeff φ)

@[simp]

theorem Polynomial.coeff_coe {R : Type u_2} [CommSemiring R] (φ : Polynomial R) (n : ℕ) : ↑(PowerSeries.coeff R n) ↑φ = Polynomial.coeff φ n

@[simp]

theorem Polynomial.coe_monomial {R : Type u_2} [CommSemiring R] (n : ℕ) (a : R) : ↑(↑(Polynomial.monomial n) a) = ↑(PowerSeries.monomial R n) a

@[simp]

theorem Polynomial.coe_zero {R : Type u_2} [CommSemiring R] : ↑0 = 0

@[simp]

theorem Polynomial.coe_one {R : Type u_2} [CommSemiring R] : ↑1 = 1

@[simp]

theorem Polynomial.coe_add {R : Type u_2} [CommSemiring R] (φ : Polynomial R) (ψ : Polynomial R) : ↑(φ + ψ) = ↑φ + ↑ψ

@[simp]

theorem Polynomial.coe_mul {R : Type u_2} [CommSemiring R] (φ : Polynomial R) (ψ : Polynomial R) : ↑(φ * ψ) = ↑φ * ↑ψ

@[simp]

theorem Polynomial.coe_C {R : Type u_2} [CommSemiring R] (a : R) : ↑(↑Polynomial.C a) = ↑(PowerSeries.C R) a

@[simp]

theorem Polynomial.coe_bit0 {R : Type u_2} [CommSemiring R] (φ : Polynomial R) : ↑(bit0 φ) = bit0 ↑φ

@[simp]

theorem Polynomial.coe_bit1 {R : Type u_2} [CommSemiring R] (φ : Polynomial R) : ↑(bit1 φ) = bit1 ↑φ

@[simp]

theorem Polynomial.coe_X {R : Type u_2} [CommSemiring R] : ↑Polynomial.X = PowerSeries.X

@[simp]

theorem Polynomial.constantCoeff_coe {R : Type u_2} [CommSemiring R] (φ : Polynomial R) : ↑(PowerSeries.constantCoeff R) ↑φ = Polynomial.coeff φ 0

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

@[simp]

theorem Polynomial.coe_inj {R : Type u_2} [CommSemiring R] {φ : Polynomial R} {ψ : Polynomial R} : ↑φ = ↑ψ ↔ φ = ψ

@[simp]

theorem Polynomial.coe_eq_zero_iff {R : Type u_2} [CommSemiring R] {φ : Polynomial R} : ↑φ = 0 ↔ φ = 0

@[simp]

theorem Polynomial.coe_eq_one_iff {R : Type u_2} [CommSemiring R] {φ : Polynomial R} : ↑φ = 1 ↔ φ = 1

def Polynomial.coeToPowerSeries.ringHom {R : Type u_2} [CommSemiring R] : Polynomial R →+* PowerSeries R

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

@[simp]

theorem Polynomial.coeToPowerSeries.ringHom_apply {R : Type u_2} [CommSemiring R] (φ : Polynomial R) : ↑Polynomial.coeToPowerSeries.ringHom φ = ↑φ

@[simp]

theorem Polynomial.coe_pow {R : Type u_2} [CommSemiring R] (φ : Polynomial R) (n : ℕ) : ↑(φ ^ n) = ↑φ ^ n

def Polynomial.coeToPowerSeries.algHom {R : Type u_2} [CommSemiring R] (A : Type u_3) [Semiring A] [Algebra R A] : Polynomial R →ₐ[R] PowerSeries A

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

@[simp]

theorem Polynomial.coeToPowerSeries.algHom_apply {R : Type u_2} [CommSemiring R] (φ : Polynomial R) (A : Type u_3) [Semiring A] [Algebra R A] : ↑(Polynomial.coeToPowerSeries.algHom A) φ = ↑(PowerSeries.map (algebraMap R A)) ↑φ

instance PowerSeries.algebraPolynomial {R : Type u_1} {A : Type u_2} [CommSemiring R] [CommSemiring A] [Algebra R A] : Algebra (Polynomial R) (PowerSeries A)

instance PowerSeries.algebraPowerSeries {R : Type u_1} {A : Type u_2} [CommSemiring R] [CommSemiring A] [Algebra R A] : Algebra (PowerSeries R) (PowerSeries A)

instance PowerSeries.algebraPolynomial' {R : Type u_1} [CommSemiring R] {A : Type u_3} [CommSemiring A] [Algebra R (Polynomial A)] : Algebra R (PowerSeries A)

theorem PowerSeries.algebraMap_apply' {R : Type u_1} (A : Type u_2) [CommSemiring R] [CommSemiring A] [Algebra R A] (p : Polynomial R) : ↑(algebraMap (Polynomial R) (PowerSeries A)) p = ↑(PowerSeries.map (algebraMap R A)) ↑p

theorem PowerSeries.algebraMap_apply'' {R : Type u_1} (A : Type u_2) [CommSemiring R] [CommSemiring A] [Algebra R A] (f : PowerSeries R) : ↑(algebraMap (PowerSeries R) (PowerSeries A)) f = ↑(PowerSeries.map (algebraMap R A)) f