Documentation

Mathlib.RingTheory.PowerSeries.Basic

Formal power series (in one variable) #

This file defines (univariate) 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.

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

The file sets up the (semi)ring structure on univariate power series.

We provide the natural inclusion from polynomials to formal power series.

Additional results can be found in:

Mathlib/RingTheory/PowerSeries/Trunc.lean, truncation of power series;
Mathlib/RingTheory/PowerSeries/Inverse.lean, about inverses of power series, and the fact that power series over a local ring form a local ring;
Mathlib/RingTheory/PowerSeries/Order.lean, the order of a power series at 0, and application to the fact that power series over an integral domain form an integral domain.

Implementation notes #

Because of its definition, PowerSeries R := MvPowerSeries Unit R. a lot of proofs and properties from the multivariate case can be ported 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 were indexed by ℕ. Occasionally this leads to proofs that are uglier than expected.

@[reducible, inline]

abbrev PowerSeries (R : Type u_1) :

Type u_1

Formal power series over a coefficient type R

Equations

PowerSeries R = MvPowerSeries Unit R

def PowerSeries.«term_⟦X⟧» :

Lean.TrailingParserDescr

R⟦X⟧ is notation for PowerSeries R, the semiring of formal power series in one variable over a semiring R.

Equations

PowerSeries.«term_⟦X⟧» = Lean.ParserDescr.trailingNode `PowerSeries.«term_⟦X⟧» 9000 0 (Lean.ParserDescr.symbol "⟦X⟧")

instance PowerSeries.instInhabited {R : Type u_1} [Inhabited R] :

Inhabited (PowerSeries R)

Equations

PowerSeries.instInhabited = id inferInstance

instance PowerSeries.instZero {R : Type u_1} [Zero R] :

Zero (PowerSeries R)

Equations

PowerSeries.instZero = id inferInstance

instance PowerSeries.instAddMonoid {R : Type u_1} [AddMonoid R] :

AddMonoid (PowerSeries R)

Equations

PowerSeries.instAddMonoid = id inferInstance

instance PowerSeries.instAddGroup {R : Type u_1} [AddGroup R] :

AddGroup (PowerSeries R)

Equations

PowerSeries.instAddGroup = id inferInstance

instance PowerSeries.instAddCommMonoid {R : Type u_1} [AddCommMonoid R] :

AddCommMonoid (PowerSeries R)

Equations

PowerSeries.instAddCommMonoid = id inferInstance

instance PowerSeries.instAddCommGroup {R : Type u_1} [AddCommGroup R] :

AddCommGroup (PowerSeries R)

Equations

PowerSeries.instAddCommGroup = id inferInstance

instance PowerSeries.instSemiring {R : Type u_1} [Semiring R] :

Semiring (PowerSeries R)

Equations

PowerSeries.instSemiring = id inferInstance

instance PowerSeries.instCommSemiring {R : Type u_1} [CommSemiring R] :

CommSemiring (PowerSeries R)

Equations

PowerSeries.instCommSemiring = id inferInstance

instance PowerSeries.instRing {R : Type u_1} [Ring R] :

Ring (PowerSeries R)

Equations

PowerSeries.instRing = id inferInstance

instance PowerSeries.instCommRing {R : Type u_1} [CommRing R] :

CommRing (PowerSeries R)

Equations

PowerSeries.instCommRing = id inferInstance

instance PowerSeries.instNontrivial {R : Type u_1} [Nontrivial R] :

Nontrivial (PowerSeries R)

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

Module R (PowerSeries A)

Equations

PowerSeries.instModule = id inferInstance

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

IsScalarTower R S (PowerSeries A)

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

Algebra R (PowerSeries A)

Equations

PowerSeries.instAlgebra = id inferInstance

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

PowerSeries R →ₗ[R] R

The nth coefficient of a formal power series.

Equations

PowerSeries.coeff R n = MvPowerSeries.coeff R (Finsupp.single () n)

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

R →ₗ[R] PowerSeries R

The nth monomial with coefficient a as formal power series.

Equations

PowerSeries.monomial R n = MvPowerSeries.monomial R (Finsupp.single () n)

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

coeff R n = MvPowerSeries.coeff R s

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

φ = ψ

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

theorem PowerSeries.ext_iff {R : Type u_1} [Semiring R] {φ ψ : PowerSeries R} :

φ = ψ ↔ ∀ (n : ℕ), (coeff R n) φ = (coeff R n) ψ

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

@[simp]

theorem PowerSeries.forall_coeff_eq_zero {R : Type u_1} [Semiring R] (φ : PowerSeries R) :

(∀ (n : ℕ), (coeff R n) φ = 0) ↔ φ = 0

instance PowerSeries.instSubsingleton {R : Type u_1} [Semiring R] [Subsingleton R] :

Subsingleton (PowerSeries R)

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

Constructor for formal power series.

Equations

PowerSeries.mk f s = f (s ())

@[simp]

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

(coeff R n) (mk f) = f n

theorem PowerSeries.coeff_monomial {R : Type u_1} [Semiring R] (m n : ℕ) (a : R) :

(coeff R m) ((monomial R n) a) = if m = n then a else 0

theorem PowerSeries.monomial_eq_mk {R : Type u_1} [Semiring R] (n : ℕ) (a : R) :

(monomial R n) a = mk fun (m : ℕ) => if m = n then a else 0

@[simp]

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

(coeff R n) ((monomial R n) a) = a

@[simp]

theorem PowerSeries.coeff_comp_monomial {R : Type u_1} [Semiring R] (n : ℕ) :

coeff R n ∘ₗ monomial R n = LinearMap.id

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

PowerSeries R →+* R

The constant coefficient of a formal power series.

Equations

PowerSeries.constantCoeff R = MvPowerSeries.constantCoeff Unit R

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

R →+* PowerSeries R

The constant formal power series.

Equations

PowerSeries.C R = MvPowerSeries.C Unit R

@[simp]

theorem PowerSeries.algebraMap_eq {R : Type u_2} [CommSemiring R] :

algebraMap R (PowerSeries R) = C R

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

The variable of the formal power series ring.

Equations

PowerSeries.X = MvPowerSeries.X ()

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

theorem PowerSeries.X_mul {R : Type u_1} [Semiring R] {φ : PowerSeries R} :

X * φ = φ * X

theorem PowerSeries.commute_X_pow {R : Type u_1} [Semiring R] (φ : PowerSeries R) (n : ℕ) :

Commute φ (X ^ n)

theorem PowerSeries.X_pow_mul {R : Type u_1} [Semiring R] {φ : PowerSeries R} {n : ℕ} :

X ^ n * φ = φ * X ^ n

@[simp]

theorem PowerSeries.coeff_zero_eq_constantCoeff {R : Type u_1} [Semiring R] :

⇑(coeff R 0) = ⇑(constantCoeff R)

theorem PowerSeries.coeff_zero_eq_constantCoeff_apply {R : Type u_1} [Semiring R] (φ : PowerSeries R) :

(coeff R 0) φ = (constantCoeff R) φ

@[simp]

theorem PowerSeries.monomial_zero_eq_C {R : Type u_1} [Semiring R] :

⇑(monomial R 0) = ⇑(C R)

theorem PowerSeries.monomial_zero_eq_C_apply {R : Type u_1} [Semiring R] (a : R) :

(monomial R 0) a = (C R) a

theorem PowerSeries.coeff_C {R : Type u_1} [Semiring R] (n : ℕ) (a : R) :

(coeff R n) ((C R) a) = if n = 0 then a else 0

@[simp]

theorem PowerSeries.coeff_zero_C {R : Type u_1} [Semiring R] (a : R) :

(coeff R 0) ((C R) a) = a

theorem PowerSeries.coeff_ne_zero_C {R : Type u_1} [Semiring R] {a : R} {n : ℕ} (h : n ≠ 0) :

(coeff R n) ((C R) a) = 0

@[simp]

theorem PowerSeries.coeff_succ_C {R : Type u_1} [Semiring R] {a : R} {n : ℕ} :

(coeff R (n + 1)) ((C R) a) = 0

theorem PowerSeries.C_injective {R : Type u_1} [Semiring R] :

Function.Injective ⇑(C R)

theorem PowerSeries.subsingleton_iff {R : Type u_1} [Semiring R] :

Subsingleton (PowerSeries R) ↔ Subsingleton R

theorem PowerSeries.X_eq {R : Type u_1} [Semiring R] :

X = (monomial R 1) 1

theorem PowerSeries.coeff_X {R : Type u_1} [Semiring R] (n : ℕ) :

(coeff R n) X = if n = 1 then 1 else 0

@[simp]

theorem PowerSeries.coeff_zero_X {R : Type u_1} [Semiring R] :

(coeff R 0) X = 0

@[simp]

theorem PowerSeries.coeff_one_X {R : Type u_1} [Semiring R] :

(coeff R 1) X = 1

@[simp]

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

theorem PowerSeries.X_pow_eq {R : Type u_1} [Semiring R] (n : ℕ) :

X ^ n = (monomial R n) 1

theorem PowerSeries.coeff_X_pow {R : Type u_1} [Semiring R] (m n : ℕ) :

(coeff R m) (X ^ n) = if m = n then 1 else 0

@[simp]

theorem PowerSeries.coeff_X_pow_self {R : Type u_1} [Semiring R] (n : ℕ) :

(coeff R n) (X ^ n) = 1

@[simp]

theorem PowerSeries.coeff_one {R : Type u_1} [Semiring R] (n : ℕ) :

(coeff R n) 1 = if n = 0 then 1 else 0

theorem PowerSeries.coeff_zero_one {R : Type u_1} [Semiring R] :

(coeff R 0) 1 = 1

theorem PowerSeries.coeff_mul {R : Type u_1} [Semiring R] (n : ℕ) (φ ψ : PowerSeries R) :

(coeff R n) (φ * ψ) = ∑ p ∈ Finset.antidiagonal n, (coeff R p.1) φ * (coeff R p.2) ψ

@[simp]

theorem PowerSeries.coeff_mul_C {R : Type u_1} [Semiring R] (n : ℕ) (φ : PowerSeries R) (a : R) :

(coeff R n) (φ * (C R) a) = (coeff R n) φ * a

@[simp]

theorem PowerSeries.coeff_C_mul {R : Type u_1} [Semiring R] (n : ℕ) (φ : PowerSeries R) (a : R) :

(coeff R n) ((C R) a * φ) = a * (coeff R n) φ

@[simp]

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

(coeff S n) (a • φ) = a • (coeff S n) φ

@[simp]

theorem PowerSeries.constantCoeff_smul {R : Type u_1} [Semiring R] {S : Type u_2} [Semiring S] [Module R S] (φ : PowerSeries S) (a : R) :

(constantCoeff S) (a • φ) = a • (constantCoeff S) φ

theorem PowerSeries.smul_eq_C_mul {R : Type u_1} [Semiring R] (f : PowerSeries R) (a : R) :

a • f = (C R) a * f

@[simp]

theorem PowerSeries.coeff_succ_mul_X {R : Type u_1} [Semiring R] (n : ℕ) (φ : PowerSeries R) :

(coeff R (n + 1)) (φ * X) = (coeff R n) φ

@[simp]

theorem PowerSeries.coeff_succ_X_mul {R : Type u_1} [Semiring R] (n : ℕ) (φ : PowerSeries R) :

(coeff R (n + 1)) (X * φ) = (coeff R n) φ

theorem PowerSeries.mul_X_cancel {R : Type u_1} [Semiring R] {φ ψ : PowerSeries R} (h : φ * X = ψ * X) :

φ = ψ

theorem PowerSeries.mul_X_injective {R : Type u_1} [Semiring R] :

Function.Injective fun (x : PowerSeries R) => x * X

theorem PowerSeries.mul_X_inj {R : Type u_1} [Semiring R] {φ ψ : PowerSeries R} :

φ * X = ψ * X ↔ φ = ψ

theorem PowerSeries.X_mul_cancel {R : Type u_1} [Semiring R] {φ ψ : PowerSeries R} (h : X * φ = X * ψ) :

φ = ψ

theorem PowerSeries.X_mul_injective {R : Type u_1} [Semiring R] :

Function.Injective fun (x : PowerSeries R) => X * x

theorem PowerSeries.X_mul_inj {R : Type u_1} [Semiring R] {φ ψ : PowerSeries R} :

X * φ = X * ψ ↔ φ = ψ

@[simp]

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

(constantCoeff R) ((C R) a) = a

@[simp]

theorem PowerSeries.constantCoeff_comp_C {R : Type u_1} [Semiring R] :

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

@[simp]

theorem PowerSeries.constantCoeff_zero {R : Type u_1} [Semiring R] :

(constantCoeff R) 0 = 0

@[simp]

theorem PowerSeries.constantCoeff_one {R : Type u_1} [Semiring R] :

(constantCoeff R) 1 = 1

@[simp]

theorem PowerSeries.constantCoeff_X {R : Type u_1} [Semiring R] :

(constantCoeff R) X = 0

@[simp]

theorem PowerSeries.constantCoeff_mk {R : Type u_1} [Semiring R] {f : ℕ → R} :

(constantCoeff R) (mk f) = f 0

theorem PowerSeries.coeff_zero_mul_X {R : Type u_1} [Semiring R] (φ : PowerSeries R) :

(coeff R 0) (φ * X) = 0

theorem PowerSeries.coeff_zero_X_mul {R : Type u_1} [Semiring R] (φ : PowerSeries R) :

(coeff R 0) (X * φ) = 0

theorem PowerSeries.constantCoeff_surj {R : Type u_1} [Semiring R] :

Function.Surjective ⇑(constantCoeff R)

theorem PowerSeries.coeff_C_mul_X_pow {R : Type u_1} [Semiring R] (x : R) (k n : ℕ) :

(coeff R n) ((C R) x * X ^ k) = if n = k then x else 0

@[simp]

theorem PowerSeries.coeff_mul_X_pow {R : Type u_1} [Semiring R] (p : PowerSeries R) (n d : ℕ) :

(coeff R (d + n)) (p * X ^ n) = (coeff R d) p

@[simp]

theorem PowerSeries.coeff_X_pow_mul {R : Type u_1} [Semiring R] (p : PowerSeries R) (n d : ℕ) :

(coeff R (d + n)) (X ^ n * p) = (coeff R d) p

theorem PowerSeries.mul_X_pow_cancel {R : Type u_1} [Semiring R] {k : ℕ} {φ ψ : PowerSeries R} (h : φ * X ^ k = ψ * X ^ k) :

φ = ψ

theorem PowerSeries.mul_X_pow_injective {R : Type u_1} [Semiring R] {k : ℕ} :

Function.Injective fun (x : PowerSeries R) => x * X ^ k

theorem PowerSeries.mul_X_pow_inj {R : Type u_1} [Semiring R] {k : ℕ} {φ ψ : PowerSeries R} :

φ * X ^ k = ψ * X ^ k ↔ φ = ψ

theorem PowerSeries.X_pow_mul_cancel {R : Type u_1} [Semiring R] {k : ℕ} {φ ψ : PowerSeries R} (h : X ^ k * φ = X ^ k * ψ) :

φ = ψ

theorem PowerSeries.X_pow_mul_injective {R : Type u_1} [Semiring R] {k : ℕ} :

Function.Injective fun (x : PowerSeries R) => X ^ k * x

theorem PowerSeries.X_pow_mul_inj {R : Type u_1} [Semiring R] {k : ℕ} {φ ψ : PowerSeries R} :

X ^ k * φ = X ^ k * ψ ↔ φ = ψ

theorem PowerSeries.coeff_mul_X_pow' {R : Type u_1} [Semiring R] (p : PowerSeries R) (n d : ℕ) :

(coeff R d) (p * X ^ n) = if n ≤ d then (coeff R (d - n)) p else 0

theorem PowerSeries.coeff_X_pow_mul' {R : Type u_1} [Semiring R] (p : PowerSeries R) (n d : ℕ) :

(coeff R d) (X ^ n * p) = if n ≤ d then (coeff R (d - n)) p else 0

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

IsUnit ((constantCoeff R) φ)

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

theorem PowerSeries.eq_shift_mul_X_add_const {R : Type u_1} [Semiring R] (φ : PowerSeries R) :

φ = (mk fun (p : ℕ) => (coeff R (p + 1)) φ) * X + (C R) ((constantCoeff R) φ)

Split off the constant coefficient.

theorem PowerSeries.eq_X_mul_shift_add_const {R : Type u_1} [Semiring R] (φ : PowerSeries R) :

φ = (X * mk fun (p : ℕ) => (coeff R (p + 1)) φ) + (C R) ((constantCoeff R) φ)

Split off the constant coefficient.

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

PowerSeries R →+* PowerSeries S

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

Equations

PowerSeries.map f = MvPowerSeries.map Unit f

@[simp]

theorem PowerSeries.map_id {R : Type u_1} [Semiring R] :

⇑(map (RingHom.id R)) = id

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

map (g.comp f) = (map g).comp (map f)

@[simp]

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

(coeff S n) ((map f) φ) = f ((coeff R n) φ)

@[simp]

theorem PowerSeries.map_C {R : Type u_1} [Semiring R] {S : Type u_2} [Semiring S] (f : R →+* S) (r : R) :

(map f) ((C R) r) = (C S) (f r)

@[simp]

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

(map f) X = X

theorem PowerSeries.map_surjective {S : Type u_2} {T : Type u_3} [Semiring S] [Semiring T] (f : S →+* T) (hf : Function.Surjective ⇑f) :

Function.Surjective ⇑(map f)

theorem PowerSeries.map_injective {S : Type u_2} {T : Type u_3} [Semiring S] [Semiring T] (f : S →+* T) (hf : Function.Injective ⇑f) :

Function.Injective ⇑(map f)

@[simp]

theorem PowerSeries.map_eq_zero {R : Type u_2} {S : Type u_3} [DivisionSemiring R] [Semiring S] [Nontrivial S] (φ : PowerSeries R) (f : R →+* S) :

(map f) φ = 0 ↔ φ = 0

theorem PowerSeries.X_pow_dvd_iff {R : Type u_1} [Semiring R] {n : ℕ} {φ : PowerSeries R} :

X ^ n ∣ φ ↔ ∀ m < n, (coeff R m) φ = 0

theorem PowerSeries.X_dvd_iff {R : Type u_1} [Semiring R] {φ : PowerSeries R} :

X ∣ φ ↔ (constantCoeff R) φ = 0

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

PowerSeries R →+* PowerSeries R

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

Equations

PowerSeries.rescale a = { toFun := fun (f : PowerSeries R) => PowerSeries.mk fun (n : ℕ) => a ^ n * (PowerSeries.coeff R n) f, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }

@[simp]

theorem PowerSeries.coeff_rescale {R : Type u_1} [CommSemiring R] (f : PowerSeries R) (a : R) (n : ℕ) :

(coeff R n) ((rescale a) f) = a ^ n * (coeff R n) f

@[simp]

theorem PowerSeries.rescale_zero {R : Type u_1} [CommSemiring R] :

rescale 0 = (C R).comp (constantCoeff R)

theorem PowerSeries.rescale_zero_apply {R : Type u_1} [CommSemiring R] (f : PowerSeries R) :

(rescale 0) f = (C R) ((constantCoeff R) f)

@[simp]

theorem PowerSeries.rescale_one {R : Type u_1} [CommSemiring R] :

rescale 1 = RingHom.id (PowerSeries R)

theorem PowerSeries.rescale_mk {R : Type u_1} [CommSemiring R] (f : ℕ → R) (a : R) :

(rescale a) (mk f) = mk fun (n : ℕ) => a ^ n * f n

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

(rescale b) ((rescale a) f) = (rescale (a * b)) f

theorem PowerSeries.rescale_mul {R : Type u_1} [CommSemiring R] (a b : R) :

rescale (a * b) = (rescale b).comp (rescale a)

theorem PowerSeries.coeff_prod {R : Type u_2} [CommSemiring R] {ι : Type u_3} [DecidableEq ι] (f : ι → PowerSeries R) (d : ℕ) (s : Finset ι) :

(coeff R d) (∏ j ∈ s, f j) = ∑ l ∈ s.finsuppAntidiag d, ∏ i ∈ s, (coeff R (l i)) (f i)

Coefficients of a product of power series

theorem PowerSeries.coeff_pow {R : Type u_2} [CommSemiring R] (k n : ℕ) (φ : PowerSeries R) :

(coeff R n) (φ ^ k) = ∑ l ∈ (Finset.range k).finsuppAntidiag n, ∏ i ∈ Finset.range k, (coeff R (l i)) φ

The n-th coefficient of the k-th power of a power series.

theorem PowerSeries.coeff_one_mul {R : Type u_2} [CommSemiring R] (φ ψ : PowerSeries R) :

(coeff R 1) (φ * ψ) = (coeff R 1) φ * (constantCoeff R) ψ + (coeff R 1) ψ * (constantCoeff R) φ

First coefficient of the product of two power series.

theorem PowerSeries.coeff_one_pow {R : Type u_2} [CommSemiring R] (n : ℕ) (φ : PowerSeries R) :

(coeff R 1) (φ ^ n) = ↑n * (coeff R 1) φ * (constantCoeff R) φ ^ (n - 1)

First coefficient of the n-th power of a power series.

theorem PowerSeries.not_isField {A : Type u_2} [CommRing A] :

¬IsField (PowerSeries A)

@[simp]

theorem PowerSeries.rescale_X {A : Type u_2} [CommRing A] (a : A) :

(rescale a) X = (C A) a * X

theorem PowerSeries.rescale_neg_one_X {A : Type u_2} [CommRing A] :

(rescale (-1)) X = -X

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

PowerSeries A →+* PowerSeries A

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

Equations

PowerSeries.evalNegHom = PowerSeries.rescale (-1)

@[simp]

theorem PowerSeries.evalNegHom_X {A : Type u_2} [CommRing A] :

evalNegHom X = -X

theorem PowerSeries.C_eq_algebraMap {R : Type u_1} [CommSemiring R] {r : R} :

(C R) r = (algebraMap R (PowerSeries R)) r

theorem PowerSeries.algebraMap_apply {R : Type u_1} {A : Type u_2} [CommSemiring R] [Semiring A] [Algebra R A] {r : R} :

(algebraMap R (PowerSeries A)) r = (C A) ((algebraMap R A) r)

instance PowerSeries.instNontrivialSubalgebra {R : Type u_1} [CommSemiring R] [Nontrivial R] :

Nontrivial (Subalgebra R (PowerSeries R))

def PowerSeries.mapAlgHom {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [Semiring A] [Algebra R A] [Semiring B] [Algebra R B] (φ : A →ₐ[R] B) :

PowerSeries A →ₐ[R] PowerSeries B

Change of coefficients in power series, as an AlgHom

Equations

PowerSeries.mapAlgHom φ = MvPowerSeries.mapAlgHom φ

theorem PowerSeries.mapAlgHom_apply {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [Semiring A] [Algebra R A] [Semiring B] [Algebra R B] (φ : A →ₐ[R] B) (f : PowerSeries A) :

(mapAlgHom φ) f = (map ↑φ) f

def Polynomial.toPowerSeries {R : Type u_1} [Semiring R] :

Polynomial R → PowerSeries R

The natural inclusion from polynomials into formal power series.

Equations

↑φ = PowerSeries.mk fun (n : ℕ) => φ.coeff n

@[deprecated Polynomial.toPowerSeries (since := "2024-10-27")]

def Polynomial.ToPowerSeries {R : Type u_1} [Semiring R] :

Polynomial R → PowerSeries R

Alias of Polynomial.toPowerSeries.

The natural inclusion from polynomials into formal power series.

Equations

@Polynomial.ToPowerSeries = @Polynomial.toPowerSeries

instance Polynomial.coeToPowerSeries {R : Type u_1} [Semiring R] :

Coe (Polynomial R) (PowerSeries R)

The natural inclusion from polynomials into formal power series.

Equations

Polynomial.coeToPowerSeries = { coe := Polynomial.toPowerSeries }

theorem Polynomial.coe_def {R : Type u_1} [Semiring R] (φ : Polynomial R) :

↑φ = PowerSeries.mk φ.coeff

@[simp]

theorem Polynomial.coeff_coe {R : Type u_1} [Semiring R] (φ : Polynomial R) (n : ℕ) :

(PowerSeries.coeff R n) ↑φ = φ.coeff n

@[simp]

theorem Polynomial.coe_monomial {R : Type u_1} [Semiring R] (n : ℕ) (a : R) :

↑((monomial n) a) = (PowerSeries.monomial R n) a

@[simp]

theorem Polynomial.coe_zero {R : Type u_1} [Semiring R] :

↑0 = 0

@[simp]

theorem Polynomial.coe_one {R : Type u_1} [Semiring R] :

↑1 = 1

@[simp]

theorem Polynomial.coe_add {R : Type u_1} [Semiring R] (φ ψ : Polynomial R) :

↑(φ + ψ) = ↑φ + ↑ψ

@[simp]

theorem Polynomial.coe_mul {R : Type u_1} [Semiring R] (φ ψ : Polynomial R) :

↑(φ * ψ) = ↑φ * ↑ψ

@[simp]

theorem Polynomial.coe_C {R : Type u_1} [Semiring R] (a : R) :

↑(C a) = (PowerSeries.C R) a

@[simp]

theorem Polynomial.coe_X {R : Type u_1} [Semiring R] :

↑X = PowerSeries.X

@[simp]

theorem Polynomial.polynomial_map_coe {U : Type u_2} {V : Type u_3} [CommSemiring U] [CommSemiring V] {φ : U →+* V} {f : Polynomial U} :

↑(map φ f) = (PowerSeries.map φ) ↑f

@[simp]

theorem Polynomial.constantCoeff_coe {R : Type u_1} [Semiring R] (φ : Polynomial R) :

(PowerSeries.constantCoeff R) ↑φ = φ.coeff 0

theorem Polynomial.coe_injective (R : Type u_1) [Semiring R] :

Function.Injective toPowerSeries

@[simp]

theorem Polynomial.coe_inj {R : Type u_1} [Semiring R] {φ ψ : Polynomial R} :

↑φ = ↑ψ ↔ φ = ψ

@[simp]

theorem Polynomial.coe_eq_zero_iff {R : Type u_1} [Semiring R] {φ : Polynomial R} :

↑φ = 0 ↔ φ = 0

@[simp]

theorem Polynomial.coe_eq_one_iff {R : Type u_1} [Semiring R] {φ : Polynomial R} :

↑φ = 1 ↔ φ = 1

def Polynomial.coeToPowerSeries.ringHom {R : Type u_1} [Semiring R] :

Polynomial R →+* PowerSeries R

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

Equations

Polynomial.coeToPowerSeries.ringHom = { toFun := Polynomial.toPowerSeries, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }

@[simp]

theorem Polynomial.coeToPowerSeries.ringHom_apply {R : Type u_1} [Semiring R] {φ : Polynomial R} :

ringHom φ = ↑φ

@[simp]

theorem Polynomial.coe_pow {R : Type u_1} [Semiring R] {φ : Polynomial R} (n : ℕ) :

↑(φ ^ n) = ↑φ ^ n

theorem Polynomial.eval₂_C_X_eq_coe {R : Type u_1} [Semiring R] {φ : Polynomial R} :

eval₂ (PowerSeries.C R) PowerSeries.X φ = ↑φ

theorem MvPolynomial.toMvPowerSeries_pUnitAlgEquiv {R : Type u_1} [CommSemiring R] {f : MvPolynomial PUnit.{1} R} :

↑f = ↑((pUnitAlgEquiv R) f)

theorem Polynomial.pUnitAlgEquiv_symm_toPowerSeries {R : Type u_1} [CommSemiring R] {f : Polynomial R} :

↑f = ↑((MvPolynomial.pUnitAlgEquiv R).symm f)

def Polynomial.coeToPowerSeries.algHom {R : Type u_1} [CommSemiring R] (A : Type u_2) [Semiring A] [Algebra R A] :

Polynomial R →ₐ[R] PowerSeries A

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

Equations

Polynomial.coeToPowerSeries.algHom A = { toRingHom := (PowerSeries.map (algebraMap R A)).comp Polynomial.coeToPowerSeries.ringHom, commutes' := ⋯ }

@[simp]

theorem Polynomial.coeToPowerSeries.algHom_apply {R : Type u_1} [CommSemiring R] (φ : Polynomial R) (A : Type u_2) [Semiring A] [Algebra R A] :

(algHom A) φ = (PowerSeries.map (algebraMap R A)) ↑φ

@[simp]

theorem Polynomial.coe_neg {R : Type u_1} [CommRing R] (p : Polynomial R) :

↑(-p) = -↑p

@[simp]

theorem Polynomial.coe_sub {R : Type u_1} [CommRing R] (p q : Polynomial R) :

↑(p - q) = ↑p - ↑q

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

Algebra (Polynomial R) (PowerSeries A)

Equations

PowerSeries.algebraPolynomial = (Polynomial.coeToPowerSeries.algHom A).toAlgebra

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

Algebra (PowerSeries R) (PowerSeries A)

Equations

PowerSeries.algebraPowerSeries = (PowerSeries.map (algebraMap R A)).toAlgebra

@[instance 100]

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

Algebra R (PowerSeries A)

Equations

PowerSeries.algebraPolynomial' = (Polynomial.coeToPowerSeries.ringHom.comp (algebraMap R (Polynomial A))).toAlgebra

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

(algebraMap (Polynomial R) (PowerSeries A)) p = (map (algebraMap R A)) ↑p

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

(algebraMap (PowerSeries R) (PowerSeries A)) f = (map (algebraMap R A)) f