mathlib documentation

ring_theory.power_series.basic

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

source
def mv_power_series (σ : Type u_1) (R : Type u_2) :
Type (max u_1 u_2)

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

Equations
source
@[protected, instance]
def mv_power_series.inhabited {σ : Type u_1} {R : Type u_2} [inhabited R] :
inhabited (mv_power_series σ R)
Equations
source
@[protected, instance]
def mv_power_series.has_zero {σ : Type u_1} {R : Type u_2} [has_zero R] :
has_zero (mv_power_series σ R)
Equations
source
@[protected, instance]
def mv_power_series.add_monoid {σ : Type u_1} {R : Type u_2} [add_monoid R] :
add_monoid (mv_power_series σ R)
Equations
source
@[protected, instance]
def mv_power_series.add_group {σ : Type u_1} {R : Type u_2} [add_group R] :
add_group (mv_power_series σ R)
Equations
source
@[protected, instance]
def mv_power_series.add_comm_monoid {σ : Type u_1} {R : Type u_2} [add_comm_monoid R] :
add_comm_monoid (mv_power_series σ R)
Equations
source
@[protected, instance]
def mv_power_series.add_comm_group {σ : Type u_1} {R : Type u_2} [add_comm_group R] :
add_comm_group (mv_power_series σ R)
Equations
source
@[protected, instance]
def mv_power_series.nontrivial {σ : Type u_1} {R : Type u_2} [nontrivial R] :
nontrivial (mv_power_series σ R)
source
@[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] :
module R (mv_power_series σ A)
Equations
source
@[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_scalar R S] [is_scalar_tower R S A] :
is_scalar_tower R S (mv_power_series σ A)
source
noncomputable def mv_power_series.monomial {σ : Type u_1} (R : Type u_2) [semiring R] (n : σ →₀ ℕ) :
R →ₗ[R] mv_power_series σ R

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

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

The nth coefficient of a multivariate formal power series.

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

source
theorem mv_power_series.ext_iff {σ : Type u_1} {R : Type u_2} [semiring R] {φ ψ : mv_power_series σ R} :
φ = ψ ↔ ∀ (n : σ →₀ ℕ), ⇑(mv_power_series.coeff R n) φ = ⇑(mv_power_series.coeff R n) ψ

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

source
theorem mv_power_series.monomial_def {σ : Type u_1} {R : Type u_2} [semiring R] [decidable_eq σ] (n : σ →₀ ℕ) :
mv_power_series.monomial R n = linear_map.std_basis R (λ (n : σ →₀ ℕ), R) n
source
theorem mv_power_series.coeff_monomial {σ : Type u_1} {R : Type u_2} [semiring R] [decidable_eq σ] (m n : σ →₀ ℕ) (a : R) :
⇑(mv_power_series.coeff R m) (⇑(mv_power_series.monomial R n) a) = ite (m = n) a 0
source
@[simp]
theorem mv_power_series.coeff_monomial_same {σ : Type u_1} {R : Type u_2} [semiring R] (n : σ →₀ ℕ) (a : R) :
⇑(mv_power_series.coeff R n) (⇑(mv_power_series.monomial R n) a) = a
source
theorem mv_power_series.coeff_monomial_ne {σ : Type u_1} {R : Type u_2} [semiring R] {m n : σ →₀ ℕ} (h : m ≠ n) (a : R) :
⇑(mv_power_series.coeff R m) (⇑(mv_power_series.monomial R n) a) = 0
source
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
source
@[simp]
theorem mv_power_series.coeff_comp_monomial {σ : Type u_1} {R : Type u_2} [semiring R] (n : σ →₀ ℕ) :
(mv_power_series.coeff R n).comp (mv_power_series.monomial R n) = linear_map.id
source
@[simp]
theorem mv_power_series.coeff_zero {σ : Type u_1} {R : Type u_2} [semiring R] (n : σ →₀ ℕ) :
⇑(mv_power_series.coeff R n) 0 = 0
source
@[protected, instance]
noncomputable def mv_power_series.has_one {σ : Type u_1} {R : Type u_2} [semiring R] :
has_one (mv_power_series σ R)
Equations
source
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
source
theorem mv_power_series.coeff_zero_one {σ : Type u_1} {R : Type u_2} [semiring R] :
⇑(mv_power_series.coeff R 0) 1 = 1
source
theorem mv_power_series.monomial_zero_one {σ : Type u_1} {R : Type u_2} [semiring R] :
⇑(mv_power_series.monomial R 0) 1 = 1
source
@[protected, instance]
noncomputable def mv_power_series.has_mul {σ : Type u_1} {R : Type u_2} [semiring R] :
has_mul (mv_power_series σ R)
Equations
source
theorem mv_power_series.coeff_mul {σ : Type u_1} {R : Type u_2} [semiring R] (n : σ →₀ ℕ) (φ ψ : mv_power_series σ R) :
⇑(mv_power_series.coeff R n) (φ * ψ) = ∑ (p : (σ →₀ ℕ) × (σ →₀ ℕ)) in n.antidiagonal, (⇑(mv_power_series.coeff R p.fst) φ) * ⇑(mv_power_series.coeff R p.snd) ψ
source
@[protected]
theorem mv_power_series.zero_mul {σ : Type u_1} {R : Type u_2} [semiring R] (φ : mv_power_series σ R) :
0 * φ = 0
source
@[protected]
theorem mv_power_series.mul_zero {σ : Type u_1} {R : Type u_2} [semiring R] (φ : mv_power_series σ R) :
φ * 0 = 0
source
theorem mv_power_series.coeff_monomial_mul {σ : Type u_1} {R : Type u_2} [semiring R] (m n : σ →₀ ℕ) (φ : mv_power_series σ R) (a : R) :
⇑(mv_power_series.coeff R m) ((⇑(mv_power_series.monomial R n) a) * φ) = ite (n ≤ m) (a * ⇑(mv_power_series.coeff R (m - n)) φ) 0
source
theorem mv_power_series.coeff_mul_monomial {σ : Type u_1} {R : Type u_2} [semiring R] (m n : σ →₀ ℕ) (φ : mv_power_series σ R) (a : R) :
⇑(mv_power_series.coeff R m) (φ * ⇑(mv_power_series.monomial R n) a) = ite (n ≤ m) ((⇑(mv_power_series.coeff R (m - n)) φ) * a) 0
source
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) :
⇑(mv_power_series.coeff R (m + n)) ((⇑(mv_power_series.monomial R m) a) * φ) = a * ⇑(mv_power_series.coeff R n) φ
source
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) :
⇑(mv_power_series.coeff R (m + n)) (φ * ⇑(mv_power_series.monomial R n) a) = (⇑(mv_power_series.coeff R m) φ) * a
source
@[protected]
theorem mv_power_series.one_mul {σ : Type u_1} {R : Type u_2} [semiring R] (φ : mv_power_series σ R) :
1 * φ = φ
source
@[protected]
theorem mv_power_series.mul_one {σ : Type u_1} {R : Type u_2} [semiring R] (φ : mv_power_series σ R) :
φ * 1 = φ
source
@[protected]
theorem mv_power_series.mul_add {σ : Type u_1} {R : Type u_2} [semiring R] (φ₁ φ₂ φ₃ : mv_power_series σ R) :
φ₁ * (φ₂ + φ₃) = φ₁ * φ₂ + φ₁ * φ₃
source
@[protected]
theorem mv_power_series.add_mul {σ : Type u_1} {R : Type u_2} [semiring R] (φ₁ φ₂ φ₃ : mv_power_series σ R) :
(φ₁ + φ₂) * φ₃ = φ₁ * φ₃ + φ₂ * φ₃
source
@[protected]
theorem mv_power_series.mul_assoc {σ : Type u_1} {R : Type u_2} [semiring R] (φ₁ φ₂ φ₃ : mv_power_series σ R) :
(φ₁ * φ₂) * φ₃ = φ₁ * φ₂ * φ₃
source
@[protected, instance]
noncomputable def mv_power_series.semiring {σ : Type u_1} {R : Type u_2} [semiring R] :
semiring (mv_power_series σ R)
Equations
source
@[protected, instance]
noncomputable def mv_power_series.comm_semiring {σ : Type u_1} {R : Type u_2} [comm_semiring R] :
comm_semiring (mv_power_series σ R)
Equations
source
@[protected, instance]
noncomputable def mv_power_series.ring {σ : Type u_1} {R : Type u_2} [ring R] :
ring (mv_power_series σ R)
Equations
source
@[protected, instance]
noncomputable def mv_power_series.comm_ring {σ : Type u_1} {R : Type u_2} [comm_ring R] :
comm_ring (mv_power_series σ R)
Equations
source
theorem mv_power_series.monomial_mul_monomial {σ : Type u_1} {R : Type u_2} [semiring R] (m n : σ →₀ ℕ) (a b : R) :
(⇑(mv_power_series.monomial R m) a) * ⇑(mv_power_series.monomial R n) b = ⇑(mv_power_series.monomial R (m + n)) (a * b)
source
noncomputable def mv_power_series.C (σ : Type u_1) (R : Type u_2) [semiring R] :
R →+* mv_power_series σ R

The constant multivariate formal power series.

Equations
source
@[simp]
theorem mv_power_series.monomial_zero_eq_C {σ : Type u_1} {R : Type u_2} [semiring R] :
⇑(mv_power_series.monomial R 0) = ⇑(mv_power_series.C σ R)
source
theorem mv_power_series.monomial_zero_eq_C_apply {σ : Type u_1} {R : Type u_2} [semiring R] (a : R) :
⇑(mv_power_series.monomial R 0) a = ⇑(mv_power_series.C σ R) a
source
theorem mv_power_series.coeff_C {σ : Type u_1} {R : Type u_2} [semiring R] [decidable_eq σ] (n : σ →₀ ℕ) (a : R) :
⇑(mv_power_series.coeff R n) (⇑(mv_power_series.C σ R) a) = ite (n = 0) a 0
source
theorem mv_power_series.coeff_zero_C {σ : Type u_1} {R : Type u_2} [semiring R] (a : R) :
⇑(mv_power_series.coeff R 0) (⇑(mv_power_series.C σ R) a) = a
source
noncomputable def mv_power_series.X {σ : Type u_1} {R : Type u_2} [semiring R] (s : σ) :
mv_power_series σ R

The variables of the multivariate formal power series ring.

Equations
source
theorem mv_power_series.coeff_X {σ : Type u_1} {R : Type u_2} [semiring R] [decidable_eq σ] (n : σ →₀ ℕ) (s : σ) :
⇑(mv_power_series.coeff R n) (mv_power_series.X s) = ite (n = finsupp.single s 1) 1 0
source
theorem mv_power_series.coeff_index_single_X {σ : Type u_1} {R : Type u_2} [semiring R] [decidable_eq σ] (s t : σ) :
⇑(mv_power_series.coeff R (finsupp.single t 1)) (mv_power_series.X s) = ite (t = s) 1 0
source
@[simp]
theorem mv_power_series.coeff_index_single_self_X {σ : Type u_1} {R : Type u_2} [semiring R] (s : σ) :
⇑(mv_power_series.coeff R (finsupp.single s 1)) (mv_power_series.X s) = 1
source
theorem mv_power_series.coeff_zero_X {σ : Type u_1} {R : Type u_2} [semiring R] (s : σ) :
⇑(mv_power_series.coeff R 0) (mv_power_series.X s) = 0
source
theorem mv_power_series.X_def {σ : Type u_1} {R : Type u_2} [semiring R] (s : σ) :
mv_power_series.X s = ⇑(mv_power_series.monomial R (finsupp.single s 1)) 1
source
theorem mv_power_series.X_pow_eq {σ : Type u_1} {R : Type u_2} [semiring R] (s : σ) (n : ℕ) :
mv_power_series.X s ^ n = ⇑(mv_power_series.monomial R (finsupp.single s n)) 1
source
theorem mv_power_series.coeff_X_pow {σ : Type u_1} {R : Type u_2} [semiring R] [decidable_eq σ] (m : σ →₀ ℕ) (s : σ) (n : ℕ) :
⇑(mv_power_series.coeff R m) (mv_power_series.X s ^ n) = ite (m = finsupp.single s n) 1 0
source
@[simp]
theorem mv_power_series.coeff_mul_C {σ : Type u_1} {R : Type u_2} [semiring R] (n : σ →₀ ℕ) (φ : mv_power_series σ R) (a : R) :
⇑(mv_power_series.coeff R n) (φ * ⇑(mv_power_series.C σ R) a) = (⇑(mv_power_series.coeff R n) φ) * a
source
@[simp]
theorem mv_power_series.coeff_C_mul {σ : Type u_1} {R : Type u_2} [semiring R] (n : σ →₀ ℕ) (φ : mv_power_series σ R) (a : R) :
⇑(mv_power_series.coeff R n) ((⇑(mv_power_series.C σ R) a) * φ) = a * ⇑(mv_power_series.coeff R n) φ
source
theorem mv_power_series.coeff_zero_mul_X {σ : Type u_1} {R : Type u_2} [semiring R] (φ : mv_power_series σ R) (s : σ) :
⇑(mv_power_series.coeff R 0) (φ * mv_power_series.X s) = 0
source
theorem mv_power_series.coeff_zero_X_mul {σ : Type u_1} {R : Type u_2} [semiring R] (φ : mv_power_series σ R) (s : σ) :
⇑(mv_power_series.coeff R 0) ((mv_power_series.X s) * φ) = 0
source
def mv_power_series.constant_coeff (σ : Type u_1) (R : Type u_2) [semiring R] :
mv_power_series σ R →+* R

The constant coefficient of a formal power series.

Equations
source
@[simp]
theorem mv_power_series.coeff_zero_eq_constant_coeff {σ : Type u_1} {R : Type u_2} [semiring R] :
⇑(mv_power_series.coeff R 0) = ⇑(mv_power_series.constant_coeff σ R)
source
theorem mv_power_series.coeff_zero_eq_constant_coeff_apply {σ : Type u_1} {R : Type u_2} [semiring R] (φ : mv_power_series σ R) :
⇑(mv_power_series.coeff R 0) φ = ⇑(mv_power_series.constant_coeff σ R) φ
source
@[simp]
theorem mv_power_series.constant_coeff_C {σ : Type u_1} {R : Type u_2} [semiring R] (a : R) :
⇑(mv_power_series.constant_coeff σ R) (⇑(mv_power_series.C σ R) a) = a
source
@[simp]
theorem mv_power_series.constant_coeff_comp_C {σ : Type u_1} {R : Type u_2} [semiring R] :
(mv_power_series.constant_coeff σ R).comp (mv_power_series.C σ R) = ring_hom.id R
source
@[simp]
theorem mv_power_series.constant_coeff_zero {σ : Type u_1} {R : Type u_2} [semiring R] :
⇑(mv_power_series.constant_coeff σ R) 0 = 0
source
@[simp]
theorem mv_power_series.constant_coeff_one {σ : Type u_1} {R : Type u_2} [semiring R] :
⇑(mv_power_series.constant_coeff σ R) 1 = 1
source
@[simp]
theorem mv_power_series.constant_coeff_X {σ : Type u_1} {R : Type u_2} [semiring R] (s : σ) :
⇑(mv_power_series.constant_coeff σ R) (mv_power_series.X s) = 0
source
theorem mv_power_series.is_unit_constant_coeff {σ : Type u_1} {R : Type u_2} [semiring R] (φ : mv_power_series σ R) (h : is_unit φ) :
is_unit (⇑(mv_power_series.constant_coeff σ R) φ)

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

source
@[simp]
theorem mv_power_series.coeff_smul {σ : Type u_1} {R : Type u_2} [semiring R] (f : mv_power_series σ R) (n : σ →₀ ℕ) (a : R) :
⇑(mv_power_series.coeff R n) (a • f) = a * ⇑(mv_power_series.coeff R n) f
source
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
source
theorem mv_power_series.X_inj {σ : Type u_1} {R : Type u_2} [semiring R] [nontrivial R] {s t : σ} :
mv_power_series.X s = mv_power_series.X t ↔ s = t
source
def mv_power_series.map (σ : Type u_1) {R : Type u_2} {S : Type u_3} [semiring R] [semiring S] (f : R →+* S) :
mv_power_series σ R →+* mv_power_series σ S

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

Equations
source
@[simp]
theorem mv_power_series.map_id {σ : Type u_1} {R : Type u_2} [semiring R] :
mv_power_series.map σ (ring_hom.id R) = ring_hom.id (mv_power_series σ R)
source
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) :
mv_power_series.map σ (g.comp f) = (mv_power_series.map σ g).comp (mv_power_series.map σ f)
source
@[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) :
⇑(mv_power_series.coeff S n) (⇑(mv_power_series.map σ f) φ) = ⇑f (⇑(mv_power_series.coeff R n) φ)
source
@[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) :
⇑(mv_power_series.constant_coeff σ S) (⇑(mv_power_series.map σ f) φ) = ⇑f (⇑(mv_power_series.constant_coeff σ R) φ)
source
@[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) :
⇑(mv_power_series.map σ f) (⇑(mv_power_series.monomial R n) a) = ⇑(mv_power_series.monomial S n) (⇑f a)
source
@[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) :
⇑(mv_power_series.map σ f) (⇑(mv_power_series.C σ R) a) = ⇑(mv_power_series.C σ S) (⇑f a)
source
@[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 : σ) :
⇑(mv_power_series.map σ f) (mv_power_series.X s) = mv_power_series.X s
source
@[protected, instance]
noncomputable def mv_power_series.algebra {σ : Type u_1} {R : Type u_2} {A : Type u_3} [comm_semiring R] [semiring A] [algebra R A] :
algebra R (mv_power_series σ A)
Equations
source
theorem mv_power_series.C_eq_algebra_map {σ : Type u_1} {R : Type u_2} [comm_semiring R] :
mv_power_series.C σ R = algebra_map R (mv_power_series σ R)
source
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} :
⇑(algebra_map R (mv_power_series σ A)) r = ⇑(mv_power_series.C σ A) (⇑(algebra_map R A) r)
source
@[protected, instance]
def mv_power_series.subalgebra.nontrivial {σ : Type u_1} {R : Type u_2} [comm_semiring R] [nonempty σ] [nontrivial R] :
nontrivial (subalgebra R (mv_power_series σ R))
source
noncomputable def mv_power_series.trunc_fun {σ : Type u_1} {R : Type u_2} [comm_semiring R] (n : σ →₀ ℕ) (φ : mv_power_series σ R) :
mv_polynomial σ R

Auxiliary definition for the truncation function.

Equations
source
theorem mv_power_series.coeff_trunc_fun {σ : Type u_1} {R : Type u_2} [comm_semiring R] (n m : σ →₀ ℕ) (φ : mv_power_series σ R) :
mv_polynomial.coeff m (mv_power_series.trunc_fun n φ) = ite (m < n) (⇑(mv_power_series.coeff R m) φ) 0
source
noncomputable def mv_power_series.trunc {σ : Type u_1} (R : Type u_2) [comm_semiring R] (n : σ →₀ ℕ) :
mv_power_series σ R →+ mv_polynomial σ R

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

Equations
source
theorem mv_power_series.coeff_trunc {σ : Type u_1} {R : Type u_2} [comm_semiring R] (n m : σ →₀ ℕ) (φ : mv_power_series σ R) :
mv_polynomial.coeff m (⇑(mv_power_series.trunc R n) φ) = ite (m < n) (⇑(mv_power_series.coeff R m) φ) 0
source
@[simp]
theorem mv_power_series.trunc_one {σ : Type u_1} {R : Type u_2} [comm_semiring R] (n : σ →₀ ℕ) (hnn : n ≠ 0) :
⇑(mv_power_series.trunc R n) 1 = 1
source
@[simp]
theorem mv_power_series.trunc_C {σ : Type u_1} {R : Type u_2} [comm_semiring R] (n : σ →₀ ℕ) (hnn : n ≠ 0) (a : R) :
⇑(mv_power_series.trunc R n) (⇑(mv_power_series.C σ R) a) = ⇑mv_polynomial.C a
source
theorem mv_power_series.X_pow_dvd_iff {σ : Type u_1} {R : Type u_2} [comm_semiring R] {s : σ} {n : ℕ} {φ : mv_power_series σ R} :
mv_power_series.X s ^ n ∣ φ ↔ ∀ (m : σ →₀ ℕ), ⇑m s < n → ⇑(mv_power_series.coeff R m) φ = 0
source
theorem mv_power_series.X_dvd_iff {σ : Type u_1} {R : Type u_2} [comm_semiring R] {s : σ} {φ : mv_power_series σ R} :
mv_power_series.X s ∣ φ ↔ ∀ (m : σ →₀ ℕ), ⇑m s = 0 → ⇑(mv_power_series.coeff R m) φ = 0
source
@[protected]
noncomputable def mv_power_series.inv.aux {σ : Type u_1} {R : Type u_2} [ring R] (a : R) (φ : mv_power_series σ 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
source
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) :
⇑(mv_power_series.coeff R n) (mv_power_series.inv.aux a φ) = ite (n = 0) a ((-a) * ∑ (x : (σ →₀ ℕ) × (σ →₀ ℕ)) in n.antidiagonal, ite (x.snd < n) ((⇑(mv_power_series.coeff R x.fst) φ) * ⇑(mv_power_series.coeff R x.snd) (mv_power_series.inv.aux a φ)) 0)
source
noncomputable def mv_power_series.inv_of_unit {σ : Type u_1} {R : Type u_2} [ring R] (φ : mv_power_series σ R) (u : Rˣ) :
mv_power_series σ R

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

Equations
source
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ˣ) :
⇑(mv_power_series.coeff R n) (φ.inv_of_unit u) = ite (n = 0) ↑u⁻¹ ((-↑u⁻¹) * ∑ (x : (σ →₀ ℕ) × (σ →₀ ℕ)) in n.antidiagonal, ite (x.snd < n) ((⇑(mv_power_series.coeff R x.fst) φ) * ⇑(mv_power_series.coeff R x.snd) (φ.inv_of_unit u)) 0)
source
@[simp]
theorem mv_power_series.constant_coeff_inv_of_unit {σ : Type u_1} {R : Type u_2} [ring R] (φ : mv_power_series σ R) (u : Rˣ) :
⇑(mv_power_series.constant_coeff σ R) (φ.inv_of_unit u) = ↑u⁻¹
source
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
source
@[protected, instance]
def mv_power_series.local_ring {σ : Type u_1} {R : Type u_2} [comm_ring R] [local_ring R] :
local_ring (mv_power_series σ R)

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

source
@[protected, instance]
def mv_power_series.map.is_local_ring_hom {σ : Type u_1} {R : Type u_2} {S : Type u_3} [comm_ring R] [comm_ring S] (f : R →+* S) [is_local_ring_hom f] :
is_local_ring_hom (mv_power_series.map σ f)

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

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

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

Equations
source
@[protected, instance]
noncomputable def mv_power_series.has_inv {σ : Type u_1} {k : Type u_3} [field k] :
has_inv (mv_power_series σ k)
Equations
source
theorem mv_power_series.coeff_inv {σ : Type u_1} {k : Type u_3} [field k] [decidable_eq σ] (n : σ →₀ ℕ) (φ : mv_power_series σ k) :
⇑(mv_power_series.coeff k n) φ⁻¹ = ite (n = 0) (⇑(mv_power_series.constant_coeff σ k) φ)⁻¹ ((-(⇑(mv_power_series.constant_coeff σ k) φ)⁻¹) * ∑ (x : (σ →₀ ℕ) × (σ →₀ ℕ)) in n.antidiagonal, ite (x.snd < n) ((⇑(mv_power_series.coeff k x.fst) φ) * ⇑(mv_power_series.coeff k x.snd) φ⁻¹) 0)
source
@[simp]
theorem mv_power_series.constant_coeff_inv {σ : Type u_1} {k : Type u_3} [field k] (φ : mv_power_series σ k) :
⇑(mv_power_series.constant_coeff σ k) φ⁻¹ = (⇑(mv_power_series.constant_coeff σ k) φ)⁻¹
source
theorem mv_power_series.inv_eq_zero {σ : Type u_1} {k : Type u_3} [field k] {φ : mv_power_series σ k} :
φ⁻¹ = 0 ↔ ⇑(mv_power_series.constant_coeff σ k) φ = 0
source
@[simp]
theorem mv_power_series.zero_inv {σ : Type u_1} {k : Type u_3} [field k] :
0⁻¹ = 0
source
@[simp]
theorem mv_power_series.inv_of_unit_eq {σ : Type u_1} {k : Type u_3} [field k] (φ : mv_power_series σ k) (h : ⇑(mv_power_series.constant_coeff σ k) φ ≠ 0) :
φ.inv_of_unit (units.mk0 (⇑(mv_power_series.constant_coeff σ k) φ) h) = φ⁻¹
source
@[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) :
φ.inv_of_unit u = φ⁻¹
source
@[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
source
@[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
source
@[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) :
φ₁ = φ₂ * φ₃⁻¹ ↔ φ₁ * φ₃ = φ₂
source
@[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
source
@[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
source
@[protected, simp]
theorem mv_power_series.mul_inv_rev {σ : Type u_1} {k : Type u_3} [field k] (φ ψ : mv_power_series σ k) :
(φ * ψ)⁻¹ = ψ⁻¹ * φ⁻¹
source
@[simp]
theorem mv_power_series.one_inv {σ : Type u_1} {k : Type u_3} [field k] :
1⁻¹ = 1
source
@[simp]
theorem mv_power_series.C_inv {σ : Type u_1} {k : Type u_3} [field k] (r : k) :
(⇑(mv_power_series.C σ k) r)⁻¹ = ⇑(mv_power_series.C σ k) r⁻¹
source
@[simp]
theorem mv_power_series.X_inv {σ : Type u_1} {k : Type u_3} [field k] (s : σ) :
(mv_power_series.X s)⁻¹ = 0
source
@[simp]
theorem mv_power_series.smul_inv {σ : Type u_1} {k : Type u_3} [field k] (r : k) (φ : mv_power_series σ k) :
(r • φ)⁻¹ = r⁻¹ • φ⁻¹
source
@[protected, instance]
def mv_polynomial.coe_to_mv_power_series {σ : Type u_1} {R : Type u_2} [comm_semiring R] :
has_coe (mv_polynomial σ R) (mv_power_series σ R)

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

Equations
source
theorem mv_polynomial.coe_def {σ : Type u_1} {R : Type u_2} [comm_semiring R] (φ : mv_polynomial σ R) :
↑φ = λ (n : σ →₀ ℕ), mv_polynomial.coeff n φ
source
@[simp, norm_cast]
theorem mv_polynomial.coeff_coe {σ : Type u_1} {R : Type u_2} [comm_semiring R] (φ : mv_polynomial σ R) (n : σ →₀ ℕ) :
⇑(mv_power_series.coeff R n) ↑φ = mv_polynomial.coeff n φ
source
@[simp, norm_cast]
theorem mv_polynomial.coe_monomial {σ : Type u_1} {R : Type u_2} [comm_semiring R] (n : σ →₀ ℕ) (a : R) :
↑(⇑(mv_polynomial.monomial n) a) = ⇑(mv_power_series.monomial R n) a
source
@[simp, norm_cast]
theorem mv_polynomial.coe_zero {σ : Type u_1} {R : Type u_2} [comm_semiring R] :
↑0 = 0
source
@[simp, norm_cast]
theorem mv_polynomial.coe_one {σ : Type u_1} {R : Type u_2} [comm_semiring R] :
↑1 = 1
source
@[simp, norm_cast]
theorem mv_polynomial.coe_add {σ : Type u_1} {R : Type u_2} [comm_semiring R] (φ ψ : mv_polynomial σ R) :
↑(φ + ψ) = ↑φ + ↑ψ
source
@[simp, norm_cast]
theorem mv_polynomial.coe_mul {σ : Type u_1} {R : Type u_2} [comm_semiring R] (φ ψ : mv_polynomial σ R) :
↑φ * ψ = (↑φ) * ↑ψ
source
@[simp, norm_cast]
theorem mv_polynomial.coe_C {σ : Type u_1} {R : Type u_2} [comm_semiring R] (a : R) :
↑(⇑mv_polynomial.C a) = ⇑(mv_power_series.C σ R) a
source
@[simp, norm_cast]
theorem mv_polynomial.coe_bit0 {σ : Type u_1} {R : Type u_2} [comm_semiring R] (φ : mv_polynomial σ R) :
↑(bit0 φ) = bit0 ↑φ
source
@[simp, norm_cast]
theorem mv_polynomial.coe_bit1 {σ : Type u_1} {R : Type u_2} [comm_semiring R] (φ : mv_polynomial σ R) :
↑(bit1 φ) = bit1 ↑φ
source
@[simp, norm_cast]
theorem mv_polynomial.coe_X {σ : Type u_1} {R : Type u_2} [comm_semiring R] (s : σ) :
↑(mv_polynomial.X s) = mv_power_series.X s
source
theorem mv_polynomial.coe_injective (σ : Type u_1) (R : Type u_2) [comm_semiring R] :
function.injective coe
source
@[simp, norm_cast]
theorem mv_polynomial.coe_inj {σ : Type u_1} {R : Type u_2} [comm_semiring R] {φ ψ : mv_polynomial σ R} :
↑φ = ↑ψ ↔ φ = ψ
source
@[simp]
theorem mv_polynomial.coe_eq_zero_iff {σ : Type u_1} {R : Type u_2} [comm_semiring R] {φ : mv_polynomial σ R} :
↑φ = 0 ↔ φ = 0
source
@[simp]
theorem mv_polynomial.coe_eq_one_iff {σ : Type u_1} {R : Type u_2} [comm_semiring R] {φ : mv_polynomial σ R} :
↑φ = 1 ↔ φ = 1
source
def mv_polynomial.coe_to_mv_power_series.ring_hom {σ : Type u_1} {R : Type u_2} [comm_semiring R] :
mv_polynomial σ R →+* mv_power_series σ R

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

Equations
source
@[simp, norm_cast]
theorem mv_polynomial.coe_pow {σ : Type u_1} {R : Type u_2} [comm_semiring R] {φ : mv_polynomial σ R} (n : ℕ) :
↑(φ ^ n) = ↑φ ^ n
source
@[simp]
theorem mv_polynomial.coe_to_mv_power_series.ring_hom_apply {σ : Type u_1} {R : Type u_2} [comm_semiring R] (φ : mv_polynomial σ R) :
⇑mv_polynomial.coe_to_mv_power_series.ring_hom φ = ↑φ
source
theorem mv_polynomial.algebra_map_apply {σ : Type u_1} {R : Type u_2} [comm_semiring R] (A : Type u_3) [comm_semiring A] [algebra R A] (r : R) :
⇑(algebra_map R (mv_polynomial σ A)) r = ⇑mv_polynomial.C (⇑(algebra_map R A) r)
source
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] :
mv_polynomial σ R →ₐ[R] mv_power_series σ A

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

Equations
source
@[simp]
theorem mv_polynomial.coe_to_mv_power_series.alg_hom_apply {σ : Type u_1} {R : Type u_2} [comm_semiring R] (φ : mv_polynomial σ R) (A : Type u_3) [comm_semiring A] [algebra R A] :
⇑(mv_polynomial.coe_to_mv_power_series.alg_hom A) φ = ⇑(mv_power_series.map σ (algebra_map R A)) ↑φ
source
@[protected, instance]
noncomputable def mv_power_series.algebra_mv_polynomial {σ : Type u_1} {R : Type u_2} {A : Type u_3} [comm_semiring R] [comm_semiring A] [algebra R A] :
algebra (mv_polynomial σ R) (mv_power_series σ A)
Equations
source
@[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] :
algebra (mv_power_series σ R) (mv_power_series σ A)
Equations
source
theorem mv_power_series.algebra_map_apply' {σ : Type u_1} {R : Type u_2} (A : Type u_3) [comm_semiring R] [comm_semiring A] [algebra R A] (p : mv_polynomial σ R) :
⇑(algebra_map (mv_polynomial σ R) (mv_power_series σ A)) p = ⇑(mv_power_series.map σ (algebra_map R A)) ↑p
source
theorem mv_power_series.algebra_map_apply'' {σ : Type u_1} {R : Type u_2} (A : Type u_3) [comm_semiring R] [comm_semiring A] [algebra R A] (f : mv_power_series σ R) :
⇑(algebra_map (mv_power_series σ R) (mv_power_series σ A)) f = ⇑(mv_power_series.map σ (algebra_map R A)) f
source
def power_series (R : Type u_1) :
Type u_1

Formal power series over the coefficient ring R.

Equations
source
@[protected, instance]
def power_series.inhabited {R : Type u_1} [inhabited R] :
inhabited (power_series R)
Equations
source
@[protected, instance]
def power_series.add_monoid {R : Type u_1} [add_monoid R] :
add_monoid (power_series R)
Equations
source
@[protected, instance]
def power_series.add_group {R : Type u_1} [add_group R] :
add_group (power_series R)
Equations
source
@[protected, instance]
def power_series.add_comm_monoid {R : Type u_1} [add_comm_monoid R] :
add_comm_monoid (power_series R)
Equations
source
@[protected, instance]
def power_series.add_comm_group {R : Type u_1} [add_comm_group R] :
add_comm_group (power_series R)
Equations
source
@[protected, instance]
noncomputable def power_series.semiring {R : Type u_1} [semiring R] :
semiring (power_series R)
Equations
source
@[protected, instance]
noncomputable def power_series.comm_semiring {R : Type u_1} [comm_semiring R] :
comm_semiring (power_series R)
Equations
source
@[protected, instance]
noncomputable def power_series.ring {R : Type u_1} [ring R] :
ring (power_series R)
Equations
source
@[protected, instance]
noncomputable def power_series.comm_ring {R : Type u_1} [comm_ring R] :
comm_ring (power_series R)
Equations
source
@[protected, instance]
def power_series.nontrivial {R : Type u_1} [nontrivial R] :
nontrivial (power_series R)
source
@[protected, instance]
def power_series.module {R : Type u_1} {A : Type u_2} [semiring R] [add_comm_monoid A] [module R A] :
module R (power_series A)
Equations
source
@[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_scalar R S] [is_scalar_tower R S A] :
is_scalar_tower R S (power_series A)
source
@[protected, instance]
noncomputable def power_series.algebra {R : Type u_1} {A : Type u_2} [semiring A] [comm_semiring R] [algebra R A] :
algebra R (power_series A)
Equations
source
noncomputable def power_series.coeff (R : Type u_1) [semiring R] (n : ℕ) :
power_series R →ₗ[R] R

The nth coefficient of a formal power series.

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

The nth monomial with coefficient a as formal power series.

Equations
source
theorem power_series.coeff_def {R : Type u_1} [semiring R] {s : unit →₀ ℕ} {n : ℕ} (h : ⇑s () = n) :
power_series.coeff R n = mv_power_series.coeff R s
source
@[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.

source
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.

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

Constructor for formal power series.

Equations
source
@[simp]
theorem power_series.coeff_mk {R : Type u_1} [semiring R] (n : ℕ) (f : ℕ → R) :
⇑(power_series.coeff R n) (power_series.mk f) = f n
source
theorem power_series.coeff_monomial {R : Type u_1} [semiring R] (m n : ℕ) (a : R) :
⇑(power_series.coeff R m) (⇑(power_series.monomial R n) a) = ite (m = n) a 0
source
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)
source
@[simp]
theorem power_series.coeff_monomial_same {R : Type u_1} [semiring R] (n : ℕ) (a : R) :
⇑(power_series.coeff R n) (⇑(power_series.monomial R n) a) = a
source
@[simp]
theorem power_series.coeff_comp_monomial {R : Type u_1} [semiring R] (n : ℕ) :
(power_series.coeff R n).comp (power_series.monomial R n) = linear_map.id
source
def power_series.constant_coeff (R : Type u_1) [semiring R] :
power_series R →+* R

The constant coefficient of a formal power series.

Equations
source
noncomputable def power_series.C (R : Type u_1) [semiring R] :
R →+* power_series R

The constant formal power series.

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

The variable of the formal power series ring.

Equations
source
@[simp]
theorem power_series.coeff_zero_eq_constant_coeff {R : Type u_1} [semiring R] :
⇑(power_series.coeff R 0) = ⇑(power_series.constant_coeff R)
source
theorem power_series.coeff_zero_eq_constant_coeff_apply {R : Type u_1} [semiring R] (φ : power_series R) :
⇑(power_series.coeff R 0) φ = ⇑(power_series.constant_coeff R) φ
source
@[simp]
theorem power_series.monomial_zero_eq_C {R : Type u_1} [semiring R] :
⇑(power_series.monomial R 0) = ⇑(power_series.C R)
source
theorem power_series.monomial_zero_eq_C_apply {R : Type u_1} [semiring R] (a : R) :
⇑(power_series.monomial R 0) a = ⇑(power_series.C R) a
source
theorem power_series.coeff_C {R : Type u_1} [semiring R] (n : ℕ) (a : R) :
⇑(power_series.coeff R n) (⇑(power_series.C R) a) = ite (n = 0) a 0
source
@[simp]
theorem power_series.coeff_zero_C {R : Type u_1} [semiring R] (a : R) :
⇑(power_series.coeff R 0) (⇑(power_series.C R) a) = a
source
theorem power_series.X_eq {R : Type u_1} [semiring R] :
power_series.X = ⇑(power_series.monomial R 1) 1
source
theorem power_series.coeff_X {R : Type u_1} [semiring R] (n : ℕ) :
⇑(power_series.coeff R n) power_series.X = ite (n = 1) 1 0
source
@[simp]
theorem power_series.coeff_zero_X {R : Type u_1} [semiring R] :
⇑(power_series.coeff R 0) power_series.X = 0
source
@[simp]
theorem power_series.coeff_one_X {R : Type u_1} [semiring R] :
⇑(power_series.coeff R 1) power_series.X = 1
source
@[simp]
theorem power_series.X_ne_zero {R : Type u_1} [semiring R] [nontrivial R] :
power_series.X ≠ 0
source
theorem power_series.X_pow_eq {R : Type u_1} [semiring R] (n : ℕ) :
power_series.X ^ n = ⇑(power_series.monomial R n) 1
source
theorem power_series.coeff_X_pow {R : Type u_1} [semiring R] (m n : ℕ) :
⇑(power_series.coeff R m) (power_series.X ^ n) = ite (m = n) 1 0
source
@[simp]
theorem power_series.coeff_X_pow_self {R : Type u_1} [semiring R] (n : ℕ) :
⇑(power_series.coeff R n) (power_series.X ^ n) = 1
source
@[simp]
theorem power_series.coeff_one {R : Type u_1} [semiring R] (n : ℕ) :
⇑(power_series.coeff R n) 1 = ite (n = 0) 1 0
source
theorem power_series.coeff_zero_one {R : Type u_1} [semiring R] :
⇑(power_series.coeff R 0) 1 = 1
source
theorem power_series.coeff_mul {R : Type u_1} [semiring R] (n : ℕ) (φ ψ : power_series R) :
⇑(power_series.coeff R n) (φ * ψ) = ∑ (p : ℕ × ℕ) in finset.nat.antidiagonal n, (⇑(power_series.coeff R p.fst) φ) * ⇑(power_series.coeff R p.snd) ψ
source
@[simp]
theorem power_series.coeff_mul_C {R : Type u_1} [semiring R] (n : ℕ) (φ : power_series R) (a : R) :
⇑(power_series.coeff R n) (φ * ⇑(power_series.C R) a) = (⇑(power_series.coeff R n) φ) * a
source
@[simp]
theorem power_series.coeff_C_mul {R : Type u_1} [semiring R] (n : ℕ) (φ : power_series R) (a : R) :
⇑(power_series.coeff R n) ((⇑(power_series.C R) a) * φ) = a * ⇑(power_series.coeff R n) φ
source
@[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) :
⇑(power_series.coeff S n) (a • φ) = a • ⇑(power_series.coeff S n) φ
source
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
source
@[simp]
theorem power_series.coeff_succ_mul_X {R : Type u_1} [semiring R] (n : ℕ) (φ : power_series R) :
⇑(power_series.coeff R (n + 1)) (φ * power_series.X) = ⇑(power_series.coeff R n) φ
source
@[simp]
theorem power_series.coeff_succ_X_mul {R : Type u_1} [semiring R] (n : ℕ) (φ : power_series R) :
⇑(power_series.coeff R (n + 1)) (power_series.X * φ) = ⇑(power_series.coeff R n) φ
source
@[simp]
theorem power_series.constant_coeff_C {R : Type u_1} [semiring R] (a : R) :
⇑(power_series.constant_coeff R) (⇑(power_series.C R) a) = a
source
@[simp]
theorem power_series.constant_coeff_comp_C {R : Type u_1} [semiring R] :
(power_series.constant_coeff R).comp (power_series.C R) = ring_hom.id R
source
@[simp]
theorem power_series.constant_coeff_zero {R : Type u_1} [semiring R] :
⇑(power_series.constant_coeff R) 0 = 0
source
@[simp]
theorem power_series.constant_coeff_one {R : Type u_1} [semiring R] :
⇑(power_series.constant_coeff R) 1 = 1
source
@[simp]
theorem power_series.constant_coeff_X {R : Type u_1} [semiring R] :
⇑(power_series.constant_coeff R) power_series.X = 0
source
theorem power_series.coeff_zero_mul_X {R : Type u_1} [semiring R] (φ : power_series R) :
⇑(power_series.coeff R 0) (φ * power_series.X) = 0
source
theorem power_series.coeff_zero_X_mul {R : Type u_1} [semiring R] (φ : power_series R) :
⇑(power_series.coeff R 0) (power_series.X * φ) = 0
source
theorem power_series.coeff_C_mul_X_pow {R : Type u_1} [semiring R] (x : R) (k n : ℕ) :
⇑(power_series.coeff R n) ((⇑(power_series.C R) x) * power_series.X ^ k) = ite (n = k) x 0
source
@[simp]
theorem power_series.coeff_mul_X_pow {R : Type u_1} [semiring R] (p : power_series R) (n d : ℕ) :
⇑(power_series.coeff R (d + n)) (p * power_series.X ^ n) = ⇑(power_series.coeff R d) p
source
@[simp]
theorem power_series.coeff_X_pow_mul {R : Type u_1} [semiring R] (p : power_series R) (n d : ℕ) :
⇑(power_series.coeff R (d + n)) ((power_series.X ^ n) * p) = ⇑(power_series.coeff R d) p
source
theorem power_series.coeff_mul_X_pow' {R : Type u_1} [semiring R] (p : power_series R) (n d : ℕ) :
⇑(power_series.coeff R d) (p * power_series.X ^ n) = ite (n ≤ d) (⇑(power_series.coeff R (d - n)) p) 0
source
theorem power_series.coeff_X_pow_mul' {R : Type u_1} [semiring R] (p : power_series R) (n d : ℕ) :
⇑(power_series.coeff R d) ((power_series.X ^ n) * p) = ite (n ≤ d) (⇑(power_series.coeff R (d - n)) p) 0
source
theorem power_series.is_unit_constant_coeff {R : Type u_1} [semiring R] (φ : power_series R) (h : is_unit φ) :
is_unit (⇑(power_series.constant_coeff R) φ)

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

source
theorem power_series.eq_shift_mul_X_add_const {R : Type u_1} [semiring R] (φ : power_series R) :
φ = (power_series.mk (λ (p : ℕ), ⇑(power_series.coeff R (p + 1)) φ)) * power_series.X + ⇑(power_series.C R) (⇑(power_series.constant_coeff R) φ)

Split off the constant coefficient.

source
theorem power_series.eq_X_mul_shift_add_const {R : Type u_1} [semiring R] (φ : power_series R) :
φ = power_series.X * power_series.mk (λ (p : ℕ), ⇑(power_series.coeff R (p + 1)) φ) + ⇑(power_series.C R) (⇑(power_series.constant_coeff R) φ)

Split off the constant coefficient.

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

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

Equations
source
@[simp]
theorem power_series.map_id {R : Type u_1} [semiring R] :
⇑(power_series.map (ring_hom.id R)) = id
source
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) :
power_series.map (g.comp f) = (power_series.map g).comp (power_series.map f)
source
@[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) :
⇑(power_series.coeff S n) (⇑(power_series.map f) φ) = ⇑f (⇑(power_series.coeff R n) φ)
source
@[simp]
theorem power_series.map_C {R : Type u_1} [semiring R] {S : Type u_2} [semiring S] (f : R →+* S) (r : R) :
⇑(power_series.map f) (⇑(power_series.C R) r) = ⇑(power_series.C S) (⇑f r)
source
@[simp]
theorem power_series.map_X {R : Type u_1} [semiring R] {S : Type u_2} [semiring S] (f : R →+* S) :
⇑(power_series.map f) power_series.X = power_series.X
source
theorem power_series.X_pow_dvd_iff {R : Type u_1} [comm_semiring R] {n : ℕ} {φ : power_series R} :
power_series.X ^ n ∣ φ ↔ ∀ (m : ℕ), m < n → ⇑(power_series.coeff R m) φ = 0
source
theorem power_series.X_dvd_iff {R : Type u_1} [comm_semiring R] {φ : power_series R} :
power_series.X ∣ φ ↔ ⇑(power_series.constant_coeff R) φ = 0
source
noncomputable def power_series.rescale {R : Type u_1} [comm_semiring R] (a : R) :
power_series R →+* power_series R

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

Equations
source
@[simp]
theorem power_series.coeff_rescale {R : Type u_1} [comm_semiring R] (f : power_series R) (a : R) (n : ℕ) :
⇑(power_series.coeff R n) (⇑(power_series.rescale a) f) = (a ^ n) * ⇑(power_series.coeff R n) f
source
@[simp]
theorem power_series.rescale_zero {R : Type u_1} [comm_semiring R] :
power_series.rescale 0 = (power_series.C R).comp (power_series.constant_coeff R)
source
theorem power_series.rescale_zero_apply {R : Type u_1} [comm_semiring R] :
⇑(power_series.rescale 0) power_series.X = ⇑(power_series.C R) (⇑(power_series.constant_coeff R) power_series.X)
source
@[simp]
theorem power_series.rescale_one {R : Type u_1} [comm_semiring R] :
power_series.rescale 1 = ring_hom.id (power_series R)
source
noncomputable def power_series.trunc {R : Type u_1} [comm_semiring R] (n : ℕ) (φ : power_series R) :
R[X]

The nth truncation of a formal power series to a polynomial

Equations
source
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
source
@[simp]
theorem power_series.trunc_zero {R : Type u_1} [comm_semiring R] (n : ℕ) :
power_series.trunc n 0 = 0
source
@[simp]
theorem power_series.trunc_one {R : Type u_1} [comm_semiring R] (n : ℕ) :
power_series.trunc (n + 1) 1 = 1
source
@[simp]
theorem power_series.trunc_C {R : Type u_1} [comm_semiring R] (n : ℕ) (a : R) :
power_series.trunc (n + 1) (⇑(power_series.C R) a) = ⇑polynomial.C a
source
@[simp]
theorem power_series.trunc_add {R : Type u_1} [comm_semiring R] (n : ℕ) (φ ψ : power_series R) :
power_series.trunc n (φ + ψ) = power_series.trunc n φ + power_series.trunc n ψ
source
@[protected]
noncomputable def power_series.inv.aux {R : Type u_1} [ring R] :
R → power_series R → power_series R

Auxiliary function used for computing inverse of a power series

Equations
source
theorem power_series.coeff_inv_aux {R : Type u_1} [ring R] (n : ℕ) (a : R) (φ : power_series R) :
⇑(power_series.coeff R n) (power_series.inv.aux a φ) = ite (n = 0) a ((-a) * ∑ (x : ℕ × ℕ) in finset.nat.antidiagonal n, ite (x.snd < n) ((⇑(power_series.coeff R x.fst) φ) * ⇑(power_series.coeff R x.snd) (power_series.inv.aux a φ)) 0)
source
noncomputable def power_series.inv_of_unit {R : Type u_1} [ring R] (φ : power_series R) (u : Rˣ) :
power_series R

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

Equations
source
theorem power_series.coeff_inv_of_unit {R : Type u_1} [ring R] (n : ℕ) (φ : power_series R) (u : Rˣ) :
⇑(power_series.coeff R n) (φ.inv_of_unit u) = ite (n = 0) ↑u⁻¹ ((-↑u⁻¹) * ∑ (x : ℕ × ℕ) in finset.nat.antidiagonal n, ite (x.snd < n) ((⇑(power_series.coeff R x.fst) φ) * ⇑(power_series.coeff R x.snd) (φ.inv_of_unit u)) 0)
source
@[simp]
theorem power_series.constant_coeff_inv_of_unit {R : Type u_1} [ring R] (φ : power_series R) (u : Rˣ) :
⇑(power_series.constant_coeff R) (φ.inv_of_unit u) = ↑u⁻¹
source
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
source
theorem power_series.sub_const_eq_shift_mul_X {R : Type u_1} [ring R] (φ : power_series R) :
φ - ⇑(power_series.C R) (⇑(power_series.constant_coeff R) φ) = (power_series.mk (λ (p : ℕ), ⇑(power_series.coeff R (p + 1)) φ)) * power_series.X

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

source
theorem power_series.sub_const_eq_X_mul_shift {R : Type u_1} [ring R] (φ : power_series R) :
φ - ⇑(power_series.C R) (⇑(power_series.constant_coeff R) φ) = power_series.X * power_series.mk (λ (p : ℕ), ⇑(power_series.coeff R (p + 1)) φ)
source
@[simp]
theorem power_series.rescale_neg_one_X {A : Type u_2} [comm_ring A] :
⇑(power_series.rescale (-1)) power_series.X = -power_series.X
source
noncomputable def power_series.eval_neg_hom {A : Type u_2} [comm_ring A] :
power_series A →+* power_series A

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

Equations
source
@[simp]
theorem power_series.eval_neg_hom_X {A : Type u_2} [comm_ring A] :
⇑power_series.eval_neg_hom power_series.X = -power_series.X
source
theorem power_series.eq_zero_or_eq_zero_of_mul_eq_zero {R : Type u_1} [ring R] [is_domain R] (φ ψ : power_series R) (h : φ * ψ = 0) :
φ = 0 ∨ ψ = 0
source
@[protected, instance]
def power_series.is_domain {R : Type u_1} [ring R] [is_domain R] :
is_domain (power_series R)
source
theorem power_series.span_X_is_prime {R : Type u_1} [comm_ring R] [is_domain R] :
(ideal.span {power_series.X}).is_prime

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

source
theorem power_series.X_prime {R : Type u_1} [comm_ring R] [is_domain R] :
prime power_series.X

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

source
theorem power_series.rescale_injective {R : Type u_1} [comm_ring R] [is_domain R] {a : R} (ha : a ≠ 0) :
function.injective ⇑(power_series.rescale a)
source
@[protected, instance]
def power_series.map.is_local_ring_hom {R : Type u_1} {S : Type u_2} [comm_ring R] [comm_ring S] (f : R →+* S) [is_local_ring_hom f] :
is_local_ring_hom (power_series.map f)
source
@[protected, instance]
def power_series.local_ring {R : Type u_1} [comm_ring R] [local_ring R] :
local_ring (power_series R)
source
theorem power_series.C_eq_algebra_map {R : Type u_1} [comm_semiring R] {r : R} :
⇑(power_series.C R) r = ⇑(algebra_map R (power_series R)) r
source
theorem power_series.algebra_map_apply {R : Type u_1} {A : Type u_2} [comm_semiring R] [semiring A] [algebra R A] {r : R} :
⇑(algebra_map R (power_series A)) r = ⇑(power_series.C A) (⇑(algebra_map R A) r)
source
@[protected, instance]
def power_series.subalgebra.nontrivial {R : Type u_1} [comm_semiring R] [nontrivial R] :
nontrivial (subalgebra R (power_series R))
source
@[protected]
noncomputable def power_series.inv {k : Type u_2} [field k] :
power_series k → power_series k

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

Equations
source
@[protected, instance]
noncomputable def power_series.has_inv {k : Type u_2} [field k] :
has_inv (power_series k)
Equations
source
theorem power_series.inv_eq_inv_aux {k : Type u_2} [field k] (φ : power_series k) :
φ⁻¹ = power_series.inv.aux (⇑(power_series.constant_coeff k) φ)⁻¹ φ
source
theorem power_series.coeff_inv {k : Type u_2} [field k] (n : ℕ) (φ : power_series k) :
⇑(power_series.coeff k n) φ⁻¹ = ite (n = 0) (⇑(power_series.constant_coeff k) φ)⁻¹ ((-(⇑(power_series.constant_coeff k) φ)⁻¹) * ∑ (x : ℕ × ℕ) in finset.nat.antidiagonal n, ite (x.snd < n) ((⇑(power_series.coeff k x.fst) φ) * ⇑(power_series.coeff k x.snd) φ⁻¹) 0)
source
@[simp]
theorem power_series.constant_coeff_inv {k : Type u_2} [field k] (φ : power_series k) :
⇑(power_series.constant_coeff k) φ⁻¹ = (⇑(power_series.constant_coeff k) φ)⁻¹
source
theorem power_series.inv_eq_zero {k : Type u_2} [field k] {φ : power_series k} :
φ⁻¹ = 0 ↔ ⇑(power_series.constant_coeff k) φ = 0
source
@[simp]
theorem power_series.zero_inv {k : Type u_2} [field k] :
0⁻¹ = 0
source
@[simp]
theorem power_series.inv_of_unit_eq {k : Type u_2} [field k] (φ : power_series k) (h : ⇑(power_series.constant_coeff k) φ ≠ 0) :
φ.inv_of_unit (units.mk0 (⇑(power_series.constant_coeff k) φ) h) = φ⁻¹
source
@[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) :
φ.inv_of_unit u = φ⁻¹
source
@[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
source
@[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
source
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) :
φ₁ = φ₂ * φ₃⁻¹ ↔ φ₁ * φ₃ = φ₂
source
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
source
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
source
@[protected, simp]
theorem power_series.mul_inv_rev {k : Type u_2} [field k] (φ ψ : power_series k) :
(φ * ψ)⁻¹ = ψ⁻¹ * φ⁻¹
source
@[simp]
theorem power_series.one_inv {k : Type u_2} [field k] :
1⁻¹ = 1
source
@[simp]
theorem power_series.C_inv {k : Type u_2} [field k] (r : k) :
(⇑(power_series.C k) r)⁻¹ = ⇑(power_series.C k) r⁻¹
source
@[simp]
theorem power_series.X_inv {k : Type u_2} [field k] :
power_series.X⁻¹ = 0
source
@[simp]
theorem power_series.smul_inv {k : Type u_2} [field k] (r : k) (φ : power_series k) :
(r • φ)⁻¹ = r⁻¹ • φ⁻¹
source
theorem power_series.exists_coeff_ne_zero_iff_ne_zero {R : Type u_1} [semiring R] {φ : power_series R} :
(∃ (n : ℕ), ⇑(power_series.coeff R n) φ ≠ 0) ↔ φ ≠ 0
source
noncomputable def power_series.order {R : Type u_1} [semiring R] (φ : power_series R) :
enat

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

Equations
source
@[simp]
theorem power_series.order_zero {R : Type u_1} [semiring R] :
0.order = ⊤

The order of the 0 power series is infinite.

source
theorem power_series.order_finite_iff_ne_zero {R : Type u_1} [semiring R] {φ : power_series R} :
φ.order.dom ↔ φ ≠ 0
source
theorem power_series.coeff_order {R : Type u_1} [semiring R] {φ : power_series R} (h : φ.order.dom) :
⇑(power_series.coeff R (φ.order.get h)) φ ≠ 0

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

source
theorem power_series.order_le {R : Type u_1} [semiring R] {φ : power_series R} (n : ℕ) (h : ⇑(power_series.coeff R n) φ ≠ 0) :
φ.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.

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

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

source
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) :
↑n ≤ φ.order

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

source
theorem power_series.le_order {R : Type u_1} [semiring R] (φ : power_series R) (n : 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.

source
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.

source
theorem power_series.order_eq {R : Type u_1} [semiring R] {φ : power_series R} {n : 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.

source
theorem power_series.le_order_add {R : Type u_1} [semiring R] (φ ψ : power_series R) :
min φ.order ψ.order ≤ (φ + ψ).order

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

source
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.

source
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.

source
theorem power_series.order_monomial {R : Type u_1} [semiring R] (n : ℕ) (a : R) [decidable (a = 0)] :
(⇑(power_series.monomial R n) a).order = ite (a = 0) ⊤ ↑n

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

source
theorem power_series.order_monomial_of_ne_zero {R : Type u_1} [semiring R] (n : ℕ) (a : R) (h : a ≠ 0) :
(⇑(power_series.monomial R n) a).order = ↑n

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

source
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.

source
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) φ
source
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) (φ * ∏ (i : ι) in s, (1 - f i)) = ⇑(power_series.coeff R k) φ
source
theorem power_series.X_pow_order_dvd {R : Type u_1} [semiring R] {φ : power_series R} (h : φ.order.dom) :
power_series.X ^ φ.order.get h ∣ φ
source
theorem power_series.order_eq_multiplicity_X {R : Type u_1} [comm_semiring R] (φ : power_series R) :
φ.order = multiplicity power_series.X φ
source
@[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.

source
@[simp]
theorem power_series.order_X {R : Type u_1} [semiring R] [nontrivial R] :
power_series.X.order = 1

The order of the formal power series X is 1.

source
@[simp]
theorem power_series.order_X_pow {R : Type u_1} [semiring R] [nontrivial R] (n : ℕ) :
(power_series.X ^ n).order = ↑n

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

source
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.

source
@[protected, instance]
def polynomial.coe_to_power_series {R : Type u_2} [comm_semiring R] :
has_coe R[X] (power_series R)

The natural inclusion from polynomials into formal power series.

Equations
source
theorem polynomial.coe_def {R : Type u_2} [comm_semiring R] (φ : R[X]) :
↑φ = power_series.mk φ.coeff
source
@[simp, norm_cast]
theorem polynomial.coeff_coe {R : Type u_2} [comm_semiring R] (φ : R[X]) (n : ℕ) :
⇑(power_series.coeff R n) ↑φ = φ.coeff n
source
@[simp, norm_cast]
theorem polynomial.coe_monomial {R : Type u_2} [comm_semiring R] (n : ℕ) (a : R) :
↑(⇑(polynomial.monomial n) a) = ⇑(power_series.monomial R n) a
source
@[simp, norm_cast]
theorem polynomial.coe_zero {R : Type u_2} [comm_semiring R] :
↑0 = 0
source
@[simp, norm_cast]
theorem polynomial.coe_one {R : Type u_2} [comm_semiring R] :
↑1 = 1
source
@[simp, norm_cast]
theorem polynomial.coe_add {R : Type u_2} [comm_semiring R] (φ ψ : R[X]) :
↑(φ + ψ) = ↑φ + ↑ψ
source
@[simp, norm_cast]
theorem polynomial.coe_mul {R : Type u_2} [comm_semiring R] (φ ψ : R[X]) :
↑φ * ψ = (↑φ) * ↑ψ
source
@[simp, norm_cast]
theorem polynomial.coe_C {R : Type u_2} [comm_semiring R] (a : R) :
↑(⇑polynomial.C a) = ⇑(power_series.C R) a
source
@[simp, norm_cast]
theorem polynomial.coe_bit0 {R : Type u_2} [comm_semiring R] (φ : R[X]) :
↑(bit0 φ) = bit0 ↑φ
source
@[simp, norm_cast]
theorem polynomial.coe_bit1 {R : Type u_2} [comm_semiring R] (φ : R[X]) :
↑(bit1 φ) = bit1 ↑φ
source
@[simp, norm_cast]
theorem polynomial.coe_X {R : Type u_2} [comm_semiring R] :
↑polynomial.X = power_series.X
source
@[simp]
theorem polynomial.constant_coeff_coe {R : Type u_2} [comm_semiring R] (φ : R[X]) :
⇑(power_series.constant_coeff R) ↑φ = φ.coeff 0
source
theorem polynomial.coe_injective (R : Type u_2) [comm_semiring R] :
function.injective coe
source
@[simp, norm_cast]
theorem polynomial.coe_inj {R : Type u_2} [comm_semiring R] {φ ψ : R[X]} :
↑φ = ↑ψ ↔ φ = ψ
source
@[simp]
theorem polynomial.coe_eq_zero_iff {R : Type u_2} [comm_semiring R] {φ : R[X]} :
↑φ = 0 ↔ φ = 0
source
@[simp]
theorem polynomial.coe_eq_one_iff {R : Type u_2} [comm_semiring R] {φ : R[X]} :
↑φ = 1 ↔ φ = 1
source
def polynomial.coe_to_power_series.ring_hom {R : Type u_2} [comm_semiring R] :
R[X] →+* power_series R

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

Equations
source
@[simp]
theorem polynomial.coe_to_power_series.ring_hom_apply {R : Type u_2} [comm_semiring R] (φ : R[X]) :
⇑polynomial.coe_to_power_series.ring_hom φ = ↑φ
source
@[simp, norm_cast]
theorem polynomial.coe_pow {R : Type u_2} [comm_semiring R] (φ : R[X]) (n : ℕ) :
↑(φ ^ n) = ↑φ ^ n
source
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] :
R[X] →ₐ[R] power_series A

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

Equations
source
@[simp]
theorem polynomial.coe_to_power_series.alg_hom_apply {R : Type u_2} [comm_semiring R] (φ : R[X]) (A : Type u_3) [semiring A] [algebra R A] :
⇑(polynomial.coe_to_power_series.alg_hom A) φ = ⇑(power_series.map (algebra_map R A)) ↑φ
source
@[protected, instance]
noncomputable def power_series.algebra_polynomial {R : Type u_1} {A : Type u_2} [comm_semiring R] [comm_semiring A] [algebra R A] :
algebra R[X] (power_series A)
Equations
source
@[protected, instance]
noncomputable def power_series.algebra_power_series {R : Type u_1} {A : Type u_2} [comm_semiring R] [comm_semiring A] [algebra R A] :
algebra (power_series R) (power_series A)
Equations
source
@[protected, instance]
noncomputable def power_series.algebra_polynomial' {R : Type u_1} [comm_semiring R] {A : Type u_2} [comm_semiring A] [algebra R A[X]] :
algebra R (power_series A)
Equations
source
theorem power_series.algebra_map_apply' {R : Type u_1} (A : Type u_2) [comm_semiring R] [comm_semiring A] [algebra R A] (p : R[X]) :
⇑(algebra_map R[X] (power_series A)) p = ⇑(power_series.map (algebra_map R A)) ↑p
source
theorem power_series.algebra_map_apply'' {R : Type u_1} (A : Type u_2) [comm_semiring R] [comm_semiring A] [algebra R A] (f : power_series R) :
⇑(algebra_map (power_series R) (power_series A)) f = ⇑(power_series.map (algebra_map R A)) f