mathlib3 documentation

ring_theory.power_series.basic

Formal power series #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 mv_power_series σ 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 power_series R := mv_power_series 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.

@[protected, instance]
def mv_power_series.inhabited {σ : Type u_1} {R : Type u_2} [inhabited R] :
Equations
@[protected, instance]
def mv_power_series.has_zero {σ : Type u_1} {R : Type u_2} [has_zero R] :
Equations
@[protected, instance]
def mv_power_series.add_monoid {σ : Type u_1} {R : Type u_2} [add_monoid R] :
Equations
@[protected, instance]
def mv_power_series.add_group {σ : Type u_1} {R : Type u_2} [add_group R] :
Equations
@[protected, instance]
def mv_power_series.nontrivial {σ : Type u_1} {R : Type u_2} [nontrivial R] :
@[protected, instance]
def mv_power_series.module {σ : Type u_1} {R : Type u_2} {A : Type u_3} [semiring R] [add_comm_monoid A] [module R A] :
Equations
@[protected, instance]
def mv_power_series.is_scalar_tower {σ : Type u_1} {R : Type u_2} {A : Type u_3} {S : Type u_4} [semiring R] [semiring S] [add_comm_monoid A] [module R A] [module S A] [has_smul R S] [is_scalar_tower R S A] :
noncomputable def mv_power_series.monomial {σ : Type u_1} (R : Type u_2) [semiring R] (n : σ →₀ ) :

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

Equations
def mv_power_series.coeff {σ : Type u_1} (R : Type u_2) [semiring R] (n : σ →₀ ) :

The nth coefficient of a multivariate formal power series.

Equations
@[ext]
theorem mv_power_series.ext {σ : Type u_1} {R : Type u_2} [semiring R] {φ ψ : mv_power_series σ R} (h : (n : σ →₀ ), (mv_power_series.coeff R n) φ = (mv_power_series.coeff R n) ψ) :
φ = ψ

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

theorem mv_power_series.ext_iff {σ : Type u_1} {R : Type u_2} [semiring R] {φ ψ : mv_power_series σ R} :

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

theorem mv_power_series.monomial_def {σ : Type u_1} {R : Type u_2} [semiring R] [decidable_eq σ] (n : σ →₀ ) :
theorem mv_power_series.coeff_monomial {σ : Type u_1} {R : Type u_2} [semiring R] [decidable_eq σ] (m n : σ →₀ ) (a : R) :
@[simp]
theorem mv_power_series.coeff_monomial_same {σ : Type u_1} {R : Type u_2} [semiring R] (n : σ →₀ ) (a : R) :
theorem mv_power_series.coeff_monomial_ne {σ : Type u_1} {R : Type u_2} [semiring R] {m n : σ →₀ } (h : m n) (a : R) :
theorem mv_power_series.eq_of_coeff_monomial_ne_zero {σ : Type u_1} {R : Type u_2} [semiring R] {m n : σ →₀ } {a : R} (h : (mv_power_series.coeff R m) ((mv_power_series.monomial R n) a) 0) :
m = n
@[simp]
theorem mv_power_series.coeff_zero {σ : Type u_1} {R : Type u_2} [semiring R] (n : σ →₀ ) :
@[protected, instance]
noncomputable def mv_power_series.has_one {σ : Type u_1} {R : Type u_2} [semiring R] :
Equations
theorem mv_power_series.coeff_one {σ : Type u_1} {R : Type u_2} [semiring R] (n : σ →₀ ) [decidable_eq σ] :
(mv_power_series.coeff R n) 1 = ite (n = 0) 1 0
theorem mv_power_series.coeff_zero_one {σ : Type u_1} {R : Type u_2} [semiring R] :
@[protected, instance]
noncomputable def mv_power_series.has_mul {σ : Type u_1} {R : Type u_2} [semiring R] :
Equations
theorem mv_power_series.coeff_mul {σ : Type u_1} {R : Type u_2} [semiring R] (n : σ →₀ ) (φ ψ : mv_power_series σ R) :
@[protected]
theorem mv_power_series.zero_mul {σ : Type u_1} {R : Type u_2} [semiring R] (φ : mv_power_series σ R) :
0 * φ = 0
@[protected]
theorem mv_power_series.mul_zero {σ : Type u_1} {R : Type u_2} [semiring R] (φ : mv_power_series σ R) :
φ * 0 = 0
theorem mv_power_series.coeff_monomial_mul {σ : Type u_1} {R : Type u_2} [semiring R] (m n : σ →₀ ) (φ : mv_power_series σ R) (a : R) :
theorem mv_power_series.coeff_mul_monomial {σ : Type u_1} {R : Type u_2} [semiring R] (m n : σ →₀ ) (φ : mv_power_series σ R) (a : R) :
theorem mv_power_series.coeff_add_monomial_mul {σ : Type u_1} {R : Type u_2} [semiring R] (m n : σ →₀ ) (φ : mv_power_series σ R) (a : R) :
theorem mv_power_series.coeff_add_mul_monomial {σ : Type u_1} {R : Type u_2} [semiring R] (m n : σ →₀ ) (φ : mv_power_series σ R) (a : R) :
@[simp]
theorem mv_power_series.commute_monomial {σ : Type u_1} {R : Type u_2} [semiring R] (φ : mv_power_series σ R) {a : R} {n : σ →₀ } :
@[protected]
theorem mv_power_series.one_mul {σ : Type u_1} {R : Type u_2} [semiring R] (φ : mv_power_series σ R) :
1 * φ = φ
@[protected]
theorem mv_power_series.mul_one {σ : Type u_1} {R : Type u_2} [semiring R] (φ : mv_power_series σ R) :
φ * 1 = φ
@[protected]
theorem mv_power_series.mul_add {σ : Type u_1} {R : Type u_2} [semiring R] (φ₁ φ₂ φ₃ : mv_power_series σ R) :
φ₁ * (φ₂ + φ₃) = φ₁ * φ₂ + φ₁ * φ₃
@[protected]
theorem mv_power_series.add_mul {σ : Type u_1} {R : Type u_2} [semiring R] (φ₁ φ₂ φ₃ : mv_power_series σ R) :
(φ₁ + φ₂) * φ₃ = φ₁ * φ₃ + φ₂ * φ₃
@[protected]
theorem mv_power_series.mul_assoc {σ : Type u_1} {R : Type u_2} [semiring R] (φ₁ φ₂ φ₃ : mv_power_series σ R) :
φ₁ * φ₂ * φ₃ = φ₁ * (φ₂ * φ₃)
@[protected, instance]
noncomputable def mv_power_series.ring {σ : Type u_1} {R : Type u_2} [ring R] :
Equations
@[protected, instance]
noncomputable def mv_power_series.comm_ring {σ : Type u_1} {R : Type u_2} [comm_ring R] :
Equations
theorem mv_power_series.monomial_mul_monomial {σ : Type u_1} {R : Type u_2} [semiring R] (m n : σ →₀ ) (a b : R) :
noncomputable def mv_power_series.C (σ : Type u_1) (R : Type u_2) [semiring R] :

The constant multivariate formal power series.

Equations
theorem mv_power_series.coeff_C {σ : Type u_1} {R : Type u_2} [semiring R] [decidable_eq σ] (n : σ →₀ ) (a : R) :
theorem mv_power_series.coeff_zero_C {σ : Type u_1} {R : Type u_2} [semiring R] (a : R) :
noncomputable def mv_power_series.X {σ : Type u_1} {R : Type u_2} [semiring R] (s : σ) :

The variables of the multivariate formal power series ring.

Equations
theorem mv_power_series.coeff_X {σ : Type u_1} {R : Type u_2} [semiring R] [decidable_eq σ] (n : σ →₀ ) (s : σ) :
theorem mv_power_series.coeff_index_single_X {σ : Type u_1} {R : Type u_2} [semiring R] [decidable_eq σ] (s t : σ) :
theorem mv_power_series.coeff_zero_X {σ : Type u_1} {R : Type u_2} [semiring R] (s : σ) :
theorem mv_power_series.commute_X {σ : Type u_1} {R : Type u_2} [semiring R] (φ : mv_power_series σ R) (s : σ) :
theorem mv_power_series.X_def {σ : Type u_1} {R : Type u_2} [semiring R] (s : σ) :
theorem mv_power_series.X_pow_eq {σ : Type u_1} {R : Type u_2} [semiring R] (s : σ) (n : ) :
theorem mv_power_series.coeff_X_pow {σ : Type u_1} {R : Type u_2} [semiring R] [decidable_eq σ] (m : σ →₀ ) (s : σ) (n : ) :
@[simp]
theorem mv_power_series.coeff_mul_C {σ : Type u_1} {R : Type u_2} [semiring R] (n : σ →₀ ) (φ : mv_power_series σ R) (a : R) :
@[simp]
theorem mv_power_series.coeff_C_mul {σ : Type u_1} {R : Type u_2} [semiring R] (n : σ →₀ ) (φ : mv_power_series σ R) (a : R) :
theorem mv_power_series.coeff_zero_mul_X {σ : Type u_1} {R : Type u_2} [semiring R] (φ : mv_power_series σ R) (s : σ) :
theorem mv_power_series.coeff_zero_X_mul {σ : Type u_1} {R : Type u_2} [semiring R] (φ : mv_power_series σ R) (s : σ) :
def mv_power_series.constant_coeff (σ : Type u_1) (R : Type u_2) [semiring R] :

The constant coefficient of a formal power series.

Equations
@[simp]
theorem mv_power_series.constant_coeff_C {σ : Type u_1} {R : Type u_2} [semiring R] (a : R) :
@[simp]
@[simp]
@[simp]
theorem mv_power_series.constant_coeff_X {σ : Type u_1} {R : Type u_2} [semiring R] (s : σ) :
theorem mv_power_series.is_unit_constant_coeff {σ : Type u_1} {R : Type u_2} [semiring R] (φ : mv_power_series σ R) (h : is_unit φ) :

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

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

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

Equations
Instances for mv_power_series.map
@[simp]
theorem mv_power_series.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) :
@[simp]
theorem mv_power_series.coeff_map {σ : Type u_1} {R : Type u_2} {S : Type u_3} [semiring R] [semiring S] (f : R →+* S) (n : σ →₀ ) (φ : mv_power_series σ R) :
@[simp]
theorem mv_power_series.constant_coeff_map {σ : Type u_1} {R : Type u_2} {S : Type u_3} [semiring R] [semiring S] (f : R →+* S) (φ : mv_power_series σ R) :
@[simp]
theorem mv_power_series.map_monomial {σ : Type u_1} {R : Type u_2} {S : Type u_3} [semiring R] [semiring S] (f : R →+* S) (n : σ →₀ ) (a : R) :
@[simp]
theorem mv_power_series.map_C {σ : Type u_1} {R : Type u_2} {S : Type u_3} [semiring R] [semiring S] (f : R →+* S) (a : R) :
@[simp]
theorem mv_power_series.map_X {σ : Type u_1} {R : Type u_2} {S : Type u_3} [semiring R] [semiring S] (f : R →+* S) (s : σ) :
theorem mv_power_series.algebra_map_apply {σ : Type u_1} {R : Type u_2} {A : Type u_3} [comm_semiring R] [semiring A] [algebra R A] {r : R} :
@[protected, instance]
noncomputable def mv_power_series.trunc_fun {σ : Type u_1} {R : Type u_2} [comm_semiring R] (n : σ →₀ ) (φ : mv_power_series σ R) :

Auxiliary definition for the truncation function.

Equations
noncomputable def mv_power_series.trunc {σ : Type u_1} (R : Type u_2) [comm_semiring R] (n : σ →₀ ) :

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

Equations
theorem mv_power_series.coeff_trunc {σ : Type u_1} {R : Type u_2} [comm_semiring R] (n m : σ →₀ ) (φ : mv_power_series σ R) :
@[simp]
theorem mv_power_series.trunc_one {σ : Type u_1} {R : Type u_2} [comm_semiring R] (n : σ →₀ ) (hnn : n 0) :
@[simp]
theorem mv_power_series.trunc_C {σ : Type u_1} {R : Type u_2} [comm_semiring R] (n : σ →₀ ) (hnn : n 0) (a : R) :
theorem mv_power_series.X_pow_dvd_iff {σ : Type u_1} {R : Type u_2} [semiring R] {s : σ} {n : } {φ : mv_power_series σ R} :
theorem mv_power_series.X_dvd_iff {σ : Type u_1} {R : Type u_2} [semiring R] {s : σ} {φ : mv_power_series σ R} :
@[protected]
noncomputable def mv_power_series.inv.aux {σ : Type u_1} {R : Type u_2} [ring R] (a : R) (φ : mv_power_series σ 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 inv_of_unit.

Equations
theorem mv_power_series.coeff_inv_aux {σ : Type u_1} {R : Type u_2} [ring R] [decidable_eq σ] (n : σ →₀ ) (a : R) (φ : mv_power_series σ R) :
noncomputable def mv_power_series.inv_of_unit {σ : Type u_1} {R : Type u_2} [ring R] (φ : mv_power_series σ R) (u : Rˣ) :

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

Equations
theorem mv_power_series.coeff_inv_of_unit {σ : Type u_1} {R : Type u_2} [ring R] [decidable_eq σ] (n : σ →₀ ) (φ : mv_power_series σ R) (u : Rˣ) :
@[simp]
theorem mv_power_series.mul_inv_of_unit {σ : Type u_1} {R : Type u_2} [ring R] (φ : mv_power_series σ R) (u : Rˣ) (h : (mv_power_series.constant_coeff σ R) φ = u) :
φ * φ.inv_of_unit u = 1
@[protected, instance]

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

@[protected, instance]

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

@[protected]
noncomputable def mv_power_series.inv {σ : Type u_1} {k : Type u_3} [field k] (φ : mv_power_series σ k) :

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

Equations
@[protected, instance]
noncomputable def mv_power_series.has_inv {σ : Type u_1} {k : Type u_3} [field k] :
Equations
theorem mv_power_series.inv_eq_zero {σ : Type u_1} {k : Type u_3} [field k] {φ : mv_power_series σ k} :
@[simp]
theorem mv_power_series.zero_inv {σ : Type u_1} {k : Type u_3} [field k] :
0⁻¹ = 0
@[simp]
@[simp]
theorem mv_power_series.inv_of_unit_eq' {σ : Type u_1} {k : Type u_3} [field k] (φ : mv_power_series σ k) (u : kˣ) (h : (mv_power_series.constant_coeff σ k) φ = u) :
@[protected, simp]
theorem mv_power_series.mul_inv_cancel {σ : Type u_1} {k : Type u_3} [field k] (φ : mv_power_series σ k) (h : (mv_power_series.constant_coeff σ k) φ 0) :
φ * φ⁻¹ = 1
@[protected, simp]
theorem mv_power_series.inv_mul_cancel {σ : Type u_1} {k : Type u_3} [field k] (φ : mv_power_series σ k) (h : (mv_power_series.constant_coeff σ k) φ 0) :
φ⁻¹ * φ = 1
@[protected]
theorem mv_power_series.eq_mul_inv_iff_mul_eq {σ : Type u_1} {k : Type u_3} [field k] {φ₁ φ₂ φ₃ : mv_power_series σ k} (h : (mv_power_series.constant_coeff σ k) φ₃ 0) :
φ₁ = φ₂ * φ₃⁻¹ φ₁ * φ₃ = φ₂
@[protected]
theorem mv_power_series.eq_inv_iff_mul_eq_one {σ : Type u_1} {k : Type u_3} [field k] {φ ψ : mv_power_series σ k} (h : (mv_power_series.constant_coeff σ k) ψ 0) :
φ = ψ⁻¹ φ * ψ = 1
@[protected]
theorem mv_power_series.inv_eq_iff_mul_eq_one {σ : Type u_1} {k : Type u_3} [field k] {φ ψ : mv_power_series σ k} (h : (mv_power_series.constant_coeff σ k) ψ 0) :
ψ⁻¹ = φ φ * ψ = 1
@[protected, simp]
theorem mv_power_series.mul_inv_rev {σ : Type u_1} {k : Type u_3} [field k] (φ ψ : mv_power_series σ k) :
* ψ)⁻¹ = ψ⁻¹ * φ⁻¹
@[protected, instance]
noncomputable def mv_power_series.inv_one_class {σ : Type u_1} {k : Type u_3} [field k] :
Equations
@[simp]
theorem mv_power_series.C_inv {σ : Type u_1} {k : Type u_3} [field k] (r : k) :
@[simp]
theorem mv_power_series.X_inv {σ : Type u_1} {k : Type u_3} [field k] (s : σ) :
@[simp]
theorem mv_power_series.smul_inv {σ : Type u_1} {k : Type u_3} [field k] (r : k) (φ : mv_power_series σ k) :
@[protected, instance]

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

Equations
theorem mv_polynomial.coe_def {σ : Type u_1} {R : Type u_2} [comm_semiring R] (φ : mv_polynomial σ R) :
φ = λ (n : σ →₀ ), mv_polynomial.coeff n φ
@[simp, norm_cast]
theorem mv_polynomial.coeff_coe {σ : Type u_1} {R : Type u_2} [comm_semiring R] (φ : mv_polynomial σ R) (n : σ →₀ ) :
@[simp, norm_cast]
theorem mv_polynomial.coe_monomial {σ : Type u_1} {R : Type u_2} [comm_semiring R] (n : σ →₀ ) (a : R) :
@[simp, norm_cast]
theorem mv_polynomial.coe_zero {σ : Type u_1} {R : Type u_2} [comm_semiring R] :
0 = 0
@[simp, norm_cast]
theorem mv_polynomial.coe_one {σ : Type u_1} {R : Type u_2} [comm_semiring R] :
1 = 1
@[simp, norm_cast]
theorem mv_polynomial.coe_add {σ : Type u_1} {R : Type u_2} [comm_semiring R] (φ ψ : mv_polynomial σ R) :
+ ψ) = φ + ψ
@[simp, norm_cast]
theorem mv_polynomial.coe_mul {σ : Type u_1} {R : Type u_2} [comm_semiring R] (φ ψ : mv_polynomial σ R) :
* ψ) = φ * ψ
@[simp, norm_cast]
theorem mv_polynomial.coe_C {σ : Type u_1} {R : Type u_2} [comm_semiring R] (a : R) :
@[simp, norm_cast]
theorem mv_polynomial.coe_bit0 {σ : Type u_1} {R : Type u_2} [comm_semiring R] (φ : mv_polynomial σ R) :
(bit0 φ) = bit0 φ
@[simp, norm_cast]
theorem mv_polynomial.coe_bit1 {σ : Type u_1} {R : Type u_2} [comm_semiring R] (φ : mv_polynomial σ R) :
(bit1 φ) = bit1 φ
@[simp, norm_cast]
theorem mv_polynomial.coe_X {σ : Type u_1} {R : Type u_2} [comm_semiring R] (s : σ) :
@[simp, norm_cast]
theorem mv_polynomial.coe_inj {σ : Type u_1} {R : Type u_2} [comm_semiring R] {φ ψ : mv_polynomial σ R} :
φ = ψ φ = ψ
@[simp]
theorem mv_polynomial.coe_eq_zero_iff {σ : Type u_1} {R : Type u_2} [comm_semiring R] {φ : mv_polynomial σ R} :
φ = 0 φ = 0
@[simp]
theorem mv_polynomial.coe_eq_one_iff {σ : Type u_1} {R : Type u_2} [comm_semiring R] {φ : mv_polynomial σ R} :
φ = 1 φ = 1

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

Equations
@[simp, norm_cast]
theorem mv_polynomial.coe_pow {σ : Type u_1} {R : Type u_2} [comm_semiring R] {φ : mv_polynomial σ R} (n : ) :
^ n) = φ ^ n
noncomputable def mv_polynomial.coe_to_mv_power_series.alg_hom {σ : Type u_1} {R : Type u_2} [comm_semiring R] (A : Type u_3) [comm_semiring A] [algebra R A] :

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

Equations
@[protected, instance]
noncomputable def mv_power_series.algebra_mv_power_series {σ : Type u_1} {R : Type u_2} {A : Type u_3} [comm_semiring R] [comm_semiring A] [algebra R A] :
Equations
@[protected, instance]
noncomputable def power_series.semiring {R : Type u_1} [semiring R] :
Equations
@[protected, instance]
noncomputable def power_series.ring {R : Type u_1} [ring R] :
Equations
@[protected, instance]
noncomputable def power_series.comm_ring {R : Type u_1} [comm_ring R] :
Equations
@[protected, instance]
@[protected, instance]
def power_series.module {R : Type u_1} {A : Type u_2} [semiring R] [add_comm_monoid A] [module R A] :
Equations
@[protected, instance]
def power_series.is_scalar_tower {R : Type u_1} {A : Type u_2} {S : Type u_3} [semiring R] [semiring S] [add_comm_monoid A] [module R A] [module S A] [has_smul R S] [is_scalar_tower R S A] :
@[protected, instance]
noncomputable def power_series.algebra {R : Type u_1} {A : Type u_2} [semiring A] [comm_semiring R] [algebra R A] :
Equations
noncomputable def power_series.coeff (R : Type u_1) [semiring R] (n : ) :

The nth coefficient of a formal power series.

Equations
noncomputable def power_series.monomial (R : Type u_1) [semiring R] (n : ) :

The nth monomial with coefficient a as formal power series.

Equations
@[ext]
theorem power_series.ext {R : Type u_1} [semiring R] {φ ψ : power_series R} (h : (n : ), (power_series.coeff R n) φ = (power_series.coeff R n) ψ) :
φ = ψ

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

theorem power_series.ext_iff {R : Type u_1} [semiring R] {φ ψ : power_series R} :
φ = ψ (n : ), (power_series.coeff R n) φ = (power_series.coeff R n) ψ

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

def power_series.mk {R : Type u_1} (f : R) :

Constructor for formal power series.

Equations
@[simp]
theorem power_series.coeff_mk {R : Type u_1} [semiring R] (n : ) (f : R) :
theorem power_series.coeff_monomial {R : Type u_1} [semiring R] (m n : ) (a : R) :
theorem power_series.monomial_eq_mk {R : Type u_1} [semiring R] (n : ) (a : R) :
(power_series.monomial R n) a = power_series.mk (λ (m : ), ite (m = n) a 0)
@[simp]
theorem power_series.coeff_monomial_same {R : Type u_1} [semiring R] (n : ) (a : R) :

The constant coefficient of a formal power series.

Equations
noncomputable def power_series.C (R : Type u_1) [semiring R] :

The constant formal power series.

Equations
noncomputable def power_series.X {R : Type u_1} [semiring R] :

The variable of the formal power series ring.

Equations
theorem power_series.coeff_C {R : Type u_1} [semiring R] (n : ) (a : R) :
@[simp]
theorem power_series.coeff_zero_C {R : Type u_1} [semiring R] (a : R) :
theorem power_series.coeff_X {R : Type u_1} [semiring R] (n : ) :
@[simp]
theorem power_series.coeff_X_pow {R : Type u_1} [semiring R] (m n : ) :
@[simp]
@[simp]
theorem power_series.coeff_one {R : Type u_1} [semiring R] (n : ) :
(power_series.coeff R n) 1 = ite (n = 0) 1 0
theorem power_series.coeff_mul {R : Type u_1} [semiring R] (n : ) (φ ψ : power_series R) :
@[simp]
theorem power_series.coeff_mul_C {R : Type u_1} [semiring R] (n : ) (φ : power_series R) (a : R) :
@[simp]
theorem power_series.coeff_C_mul {R : Type u_1} [semiring R] (n : ) (φ : power_series R) (a : R) :
@[simp]
theorem power_series.coeff_smul {R : Type u_1} [semiring R] {S : Type u_2} [semiring S] [module R S] (n : ) (φ : power_series S) (a : R) :
theorem power_series.smul_eq_C_mul {R : Type u_1} [semiring R] (f : power_series R) (a : R) :
a f = (power_series.C R) a * f
@[simp]
@[simp]
theorem power_series.coeff_C_mul_X_pow {R : Type u_1} [semiring R] (x : R) (k n : ) :
@[simp]
theorem power_series.coeff_mul_X_pow {R : Type u_1} [semiring R] (p : power_series R) (n d : ) :
@[simp]
theorem power_series.coeff_X_pow_mul {R : Type u_1} [semiring R] (p : power_series R) (n d : ) :
theorem power_series.coeff_mul_X_pow' {R : Type u_1} [semiring R] (p : power_series R) (n d : ) :
theorem power_series.coeff_X_pow_mul' {R : Type u_1} [semiring R] (p : power_series R) (n d : ) :

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

Split off the constant coefficient.

Split off the constant coefficient.

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

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

Equations
Instances for power_series.map
@[simp]
theorem power_series.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) :
@[simp]
theorem power_series.coeff_map {R : Type u_1} [semiring R] {S : Type u_2} [semiring S] (f : R →+* S) (n : ) (φ : power_series R) :
@[simp]
theorem power_series.map_C {R : Type u_1} [semiring R] {S : Type u_2} [semiring S] (f : R →+* S) (r : R) :
@[simp]
theorem power_series.map_X {R : Type u_1} [semiring R] {S : Type u_2} [semiring S] (f : R →+* S) :
theorem power_series.X_pow_dvd_iff {R : Type u_1} [semiring R] {n : } {φ : power_series R} :
power_series.X ^ n φ (m : ), m < n (power_series.coeff R m) φ = 0
noncomputable def power_series.rescale {R : Type u_1} [comm_semiring R] (a : R) :

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

Equations
@[simp]
theorem power_series.coeff_rescale {R : Type u_1} [comm_semiring R] (f : power_series R) (a : R) (n : ) :
theorem power_series.rescale_mk {R : Type u_1} [comm_semiring R] (f : R) (a : R) :
noncomputable def power_series.trunc {R : Type u_1} [comm_semiring R] (n : ) (φ : power_series R) :

The nth truncation of a formal power series to a polynomial

Equations
theorem power_series.coeff_trunc {R : Type u_1} [comm_semiring R] (m n : ) (φ : power_series R) :
(power_series.trunc n φ).coeff m = ite (m < n) ((power_series.coeff R m) φ) 0
@[simp]
theorem power_series.trunc_zero {R : Type u_1} [comm_semiring R] (n : ) :
@[simp]
theorem power_series.trunc_one {R : Type u_1} [comm_semiring R] (n : ) :
@[simp]
theorem power_series.trunc_C {R : Type u_1} [comm_semiring R] (n : ) (a : R) :
@[simp]
theorem power_series.trunc_add {R : Type u_1} [comm_semiring R] (n : ) (φ ψ : power_series R) :
@[protected]
noncomputable def power_series.inv.aux {R : Type u_1} [ring R] :

Auxiliary function used for computing inverse of a power series

Equations
theorem power_series.coeff_inv_aux {R : Type u_1} [ring R] (n : ) (a : R) (φ : power_series R) :
noncomputable def power_series.inv_of_unit {R : Type u_1} [ring R] (φ : power_series R) (u : Rˣ) :

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

Equations
theorem power_series.coeff_inv_of_unit {R : Type u_1} [ring R] (n : ) (φ : power_series R) (u : Rˣ) :
theorem power_series.mul_inv_of_unit {R : Type u_1} [ring R] (φ : power_series R) (u : Rˣ) (h : (power_series.constant_coeff R) φ = u) :
φ * φ.inv_of_unit u = 1

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

noncomputable def power_series.eval_neg_hom {A : Type u_2} [comm_ring A] :

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

Equations
theorem power_series.eq_zero_or_eq_zero_of_mul_eq_zero {R : Type u_1} [ring R] [no_zero_divisors R] (φ ψ : power_series R) (h : φ * ψ = 0) :
φ = 0 ψ = 0
@[protected, instance]
@[protected, instance]

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

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

@[protected, instance]
@[protected, instance]
theorem power_series.algebra_map_apply {R : Type u_1} {A : Type u_2} [comm_semiring R] [semiring A] [algebra R A] {r : R} :
@[protected]
noncomputable def power_series.inv {k : Type u_2} [field k] :

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

Equations
@[protected, instance]
noncomputable def power_series.has_inv {k : Type u_2} [field k] :
Equations
@[simp]
theorem power_series.zero_inv {k : Type u_2} [field k] :
0⁻¹ = 0
@[simp]
theorem power_series.inv_of_unit_eq' {k : Type u_2} [field k] (φ : power_series k) (u : kˣ) (h : (power_series.constant_coeff k) φ = u) :
@[protected, simp]
theorem power_series.mul_inv_cancel {k : Type u_2} [field k] (φ : power_series k) (h : (power_series.constant_coeff k) φ 0) :
φ * φ⁻¹ = 1
@[protected, simp]
theorem power_series.inv_mul_cancel {k : Type u_2} [field k] (φ : power_series k) (h : (power_series.constant_coeff k) φ 0) :
φ⁻¹ * φ = 1
theorem power_series.eq_mul_inv_iff_mul_eq {k : Type u_2} [field k] {φ₁ φ₂ φ₃ : power_series k} (h : (power_series.constant_coeff k) φ₃ 0) :
φ₁ = φ₂ * φ₃⁻¹ φ₁ * φ₃ = φ₂
theorem power_series.eq_inv_iff_mul_eq_one {k : Type u_2} [field k] {φ ψ : power_series k} (h : (power_series.constant_coeff k) ψ 0) :
φ = ψ⁻¹ φ * ψ = 1
theorem power_series.inv_eq_iff_mul_eq_one {k : Type u_2} [field k] {φ ψ : power_series k} (h : (power_series.constant_coeff k) ψ 0) :
ψ⁻¹ = φ φ * ψ = 1
@[protected, simp]
theorem power_series.mul_inv_rev {k : Type u_2} [field k] (φ ψ : power_series k) :
* ψ)⁻¹ = ψ⁻¹ * φ⁻¹
@[protected, instance]
noncomputable def power_series.inv_one_class {k : Type u_2} [field k] :
Equations
@[simp]
theorem power_series.C_inv {k : Type u_2} [field k] (r : k) :
@[simp]
theorem power_series.X_inv {k : Type u_2} [field k] :
@[simp]
theorem power_series.smul_inv {k : Type u_2} [field k] (r : k) (φ : power_series k) :
noncomputable def power_series.order {R : Type u_1} [semiring R] (φ : power_series R) :

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

Equations
@[simp]
theorem power_series.order_zero {R : Type u_1} [semiring R] :

The order of the 0 power series is infinite.

theorem power_series.coeff_order {R : Type u_1} [semiring R] {φ : power_series R} (h : φ.order.dom) :

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

theorem power_series.order_le {R : Type u_1} [semiring R] {φ : power_series R} (n : ) (h : (power_series.coeff R n) φ 0) :

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 power_series.coeff_of_lt_order {R : Type u_1} [semiring R] {φ : power_series R} (n : ) (h : n < φ.order) :

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

@[simp]
theorem power_series.order_eq_top {R : Type u_1} [semiring R] {φ : power_series R} :
φ.order = φ = 0

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

theorem power_series.nat_le_order {R : Type u_1} [semiring R] (φ : power_series R) (n : ) (h : (i : ), i < n (power_series.coeff R i) φ = 0) :

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

theorem power_series.le_order {R : Type u_1} [semiring R] (φ : power_series R) (n : part_enat) (h : (i : ), i < n (power_series.coeff R i) φ = 0) :
n φ.order

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

theorem power_series.order_eq_nat {R : Type u_1} [semiring R] {φ : power_series R} {n : } :
φ.order = n (power_series.coeff R n) φ 0 (i : ), i < n (power_series.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 power_series.order_eq {R : Type u_1} [semiring R] {φ : power_series R} {n : part_enat} :
φ.order = n ( (i : ), i = n (power_series.coeff R i) φ 0) (i : ), i < n (power_series.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 power_series.le_order_add {R : Type u_1} [semiring R] (φ ψ : power_series R) :

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

theorem power_series.order_add_of_order_eq {R : Type u_1} [semiring R] (φ ψ : power_series R) (h : φ.order ψ.order) :
+ ψ).order = φ.order ψ.order

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

theorem power_series.order_mul_ge {R : Type u_1} [semiring R] (φ ψ : power_series R) :
φ.order + ψ.order * ψ).order

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

theorem power_series.order_monomial {R : Type u_1} [semiring R] (n : ) (a : R) [decidable (a = 0)] :

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

theorem power_series.order_monomial_of_ne_zero {R : Type u_1} [semiring R] (n : ) (a : R) (h : a 0) :

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

theorem power_series.coeff_mul_of_lt_order {R : Type u_1} [semiring R] {φ ψ : power_series R} {n : } (h : n < ψ.order) :
(power_series.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 power_series.coeff_mul_one_sub_of_lt_order {R : Type u_1} [comm_ring R] {φ ψ : power_series R} (n : ) (h : n < ψ.order) :
(power_series.coeff R n) * (1 - ψ)) = (power_series.coeff R n) φ
theorem power_series.coeff_mul_prod_one_sub_of_lt_order {R : Type u_1} {ι : Type u_2} [comm_ring R] (k : ) (s : finset ι) (φ : power_series R) (f : ι power_series R) :
( (i : ι), i s k < (f i).order) (power_series.coeff R k) * s.prod (λ (i : ι), 1 - f i)) = (power_series.coeff R k) φ
theorem power_series.X_pow_order_dvd {R : Type u_1} [semiring R] {φ : power_series R} (h : φ.order.dom) :
@[simp]
theorem power_series.order_one {R : Type u_1} [semiring R] [nontrivial R] :
1.order = 0

The order of the formal power series 1 is 0.

@[simp]

The order of the formal power series X is 1.

@[simp]
theorem power_series.order_X_pow {R : Type u_1} [semiring R] [nontrivial R] (n : ) :

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

theorem power_series.order_mul {R : Type u_1} [comm_ring R] [is_domain R] (φ ψ : power_series R) :
* ψ).order = φ.order + ψ.order

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

@[protected, instance]

The natural inclusion from polynomials into formal power series.

Equations
@[simp, norm_cast]
theorem polynomial.coeff_coe {R : Type u_2} [comm_semiring R] (φ : polynomial R) (n : ) :
@[simp, norm_cast]
theorem polynomial.coe_monomial {R : Type u_2} [comm_semiring R] (n : ) (a : R) :
@[simp, norm_cast]
theorem polynomial.coe_zero {R : Type u_2} [comm_semiring R] :
0 = 0
@[simp, norm_cast]
theorem polynomial.coe_one {R : Type u_2} [comm_semiring R] :
1 = 1
@[simp, norm_cast]
theorem polynomial.coe_add {R : Type u_2} [comm_semiring R] (φ ψ : polynomial R) :
+ ψ) = φ + ψ
@[simp, norm_cast]
theorem polynomial.coe_mul {R : Type u_2} [comm_semiring R] (φ ψ : polynomial R) :
* ψ) = φ * ψ
@[simp, norm_cast]
theorem polynomial.coe_C {R : Type u_2} [comm_semiring R] (a : R) :
@[simp, norm_cast]
theorem polynomial.coe_bit0 {R : Type u_2} [comm_semiring R] (φ : polynomial R) :
(bit0 φ) = bit0 φ
@[simp, norm_cast]
theorem polynomial.coe_bit1 {R : Type u_2} [comm_semiring R] (φ : polynomial R) :
(bit1 φ) = bit1 φ
@[simp, norm_cast]
@[simp, norm_cast]
theorem polynomial.coe_inj {R : Type u_2} [comm_semiring R] {φ ψ : polynomial R} :
φ = ψ φ = ψ
@[simp]
theorem polynomial.coe_eq_zero_iff {R : Type u_2} [comm_semiring R] {φ : polynomial R} :
φ = 0 φ = 0
@[simp]
theorem polynomial.coe_eq_one_iff {R : Type u_2} [comm_semiring R] {φ : polynomial R} :
φ = 1 φ = 1

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

Equations
@[simp, norm_cast]
theorem polynomial.coe_pow {R : Type u_2} [comm_semiring R] (φ : polynomial R) (n : ) :
^ n) = φ ^ n
noncomputable def polynomial.coe_to_power_series.alg_hom {R : Type u_2} [comm_semiring R] (A : Type u_3) [semiring A] [algebra R A] :

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

Equations