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, truncation of power series;Mathlib.RingTheory.PowerSeries.Inverse, about inverses of power series, and the fact that power series over a local ring form a local ring;Mathlib.RingTheory.PowerSeries.Order, 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.
Formal power series over a coefficient type R
Equations
Instances For
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⟧")
Instances For
instance
PowerSeries.instInhabitedPowerSeries
{R : Type u_1}
[Inhabited R]
:
Inhabited (PowerSeries R)
instance
PowerSeries.instAddMonoidPowerSeries
{R : Type u_1}
[AddMonoid R]
:
AddMonoid (PowerSeries R)
Equations
- ⋯ = ⋯
instance
PowerSeries.instModulePowerSeriesInstAddCommMonoidPowerSeries
{R : Type u_1}
{A : Type u_2}
[Semiring R]
[AddCommMonoid A]
[Module R A]
:
Module R (PowerSeries A)
instance
PowerSeries.instIsScalarTowerPowerSeriesToSMulInstZeroPowerSeriesToZeroToAddMonoidToSMulZeroClassToZeroToMonoidWithZeroToSMulWithZeroToMulActionWithZeroInstAddCommMonoidPowerSeriesInstModulePowerSeriesInstAddCommMonoidPowerSeriesToSMulToSMulZeroClassToZeroToMonoidWithZeroToSMulWithZeroToMulActionWithZeroInstModulePowerSeriesInstAddCommMonoidPowerSeries
{R : Type u_1}
{A : Type u_2}
{S : Type u_3}
[Semiring R]
[Semiring S]
[AddCommMonoid A]
[Module R A]
[Module S A]
[SMul R S]
[IsScalarTower R S A]
:
IsScalarTower R S (PowerSeries A)
Equations
- ⋯ = ⋯
instance
PowerSeries.instAlgebraPowerSeriesInstSemiringPowerSeries
{R : Type u_1}
{A : Type u_2}
[Semiring A]
[CommSemiring R]
[Algebra R A]
:
Algebra R (PowerSeries A)
The nth coefficient of a formal power series.
Equations
- PowerSeries.coeff R n = MvPowerSeries.coeff R (Finsupp.single () n)
Instances For
The nth monomial with coefficient a as formal power series.
Equations
Instances For
theorem
PowerSeries.coeff_def
{R : Type u_1}
[Semiring R]
{s : Unit →₀ ℕ}
{n : ℕ}
(h : s () = n)
:
PowerSeries.coeff R n = MvPowerSeries.coeff R s
theorem
PowerSeries.ext
{R : Type u_1}
[Semiring R]
{φ : PowerSeries R}
{ψ : PowerSeries R}
(h : ∀ (n : ℕ), (PowerSeries.coeff R n) φ = (PowerSeries.coeff R n) ψ)
:
φ = ψ
Two formal power series are equal if all their coefficients are equal.
theorem
PowerSeries.ext_iff
{R : Type u_1}
[Semiring R]
{φ : PowerSeries R}
{ψ : PowerSeries R}
:
φ = ψ ↔ ∀ (n : ℕ), (PowerSeries.coeff R n) φ = (PowerSeries.coeff R n) ψ
Two formal power series are equal if all their coefficients are equal.
Equations
- ⋯ = ⋯
@[simp]
theorem
PowerSeries.coeff_mk
{R : Type u_1}
[Semiring R]
(n : ℕ)
(f : ℕ → R)
:
(PowerSeries.coeff R n) (PowerSeries.mk f) = f n
theorem
PowerSeries.coeff_monomial
{R : Type u_1}
[Semiring R]
(m : ℕ)
(n : ℕ)
(a : R)
:
(PowerSeries.coeff R m) ((PowerSeries.monomial R n) a) = if m = n then a else 0
theorem
PowerSeries.monomial_eq_mk
{R : Type u_1}
[Semiring R]
(n : ℕ)
(a : R)
:
(PowerSeries.monomial R n) a = PowerSeries.mk fun (m : ℕ) => if m = n then a else 0
@[simp]
theorem
PowerSeries.coeff_monomial_same
{R : Type u_1}
[Semiring R]
(n : ℕ)
(a : R)
:
(PowerSeries.coeff R n) ((PowerSeries.monomial R n) a) = a
@[simp]
theorem
PowerSeries.coeff_comp_monomial
{R : Type u_1}
[Semiring R]
(n : ℕ)
:
PowerSeries.coeff R n ∘ₗ PowerSeries.monomial R n = LinearMap.id
The constant coefficient of a formal power series.
Equations
Instances For
The constant formal power series.
Equations
Instances For
The variable of the formal power series ring.
Equations
- PowerSeries.X = MvPowerSeries.X ()
Instances For
theorem
PowerSeries.commute_X
{R : Type u_1}
[Semiring R]
(φ : PowerSeries R)
:
Commute φ PowerSeries.X
@[simp]
theorem
PowerSeries.coeff_zero_eq_constantCoeff
{R : Type u_1}
[Semiring R]
:
⇑(PowerSeries.coeff R 0) = ⇑(PowerSeries.constantCoeff R)
theorem
PowerSeries.coeff_zero_eq_constantCoeff_apply
{R : Type u_1}
[Semiring R]
(φ : PowerSeries R)
:
(PowerSeries.coeff R 0) φ = (PowerSeries.constantCoeff R) φ
@[simp]
theorem
PowerSeries.monomial_zero_eq_C
{R : Type u_1}
[Semiring R]
:
⇑(PowerSeries.monomial R 0) = ⇑(PowerSeries.C R)
theorem
PowerSeries.monomial_zero_eq_C_apply
{R : Type u_1}
[Semiring R]
(a : R)
:
(PowerSeries.monomial R 0) a = (PowerSeries.C R) a
theorem
PowerSeries.coeff_C
{R : Type u_1}
[Semiring R]
(n : ℕ)
(a : R)
:
(PowerSeries.coeff R n) ((PowerSeries.C R) a) = if n = 0 then a else 0
@[simp]
theorem
PowerSeries.coeff_zero_C
{R : Type u_1}
[Semiring R]
(a : R)
:
(PowerSeries.coeff R 0) ((PowerSeries.C R) a) = a
theorem
PowerSeries.coeff_ne_zero_C
{R : Type u_1}
[Semiring R]
{a : R}
{n : ℕ}
(h : n ≠ 0)
:
(PowerSeries.coeff R n) ((PowerSeries.C R) a) = 0
@[simp]
theorem
PowerSeries.coeff_succ_C
{R : Type u_1}
[Semiring R]
{a : R}
{n : ℕ}
:
(PowerSeries.coeff R (n + 1)) ((PowerSeries.C R) a) = 0
theorem
PowerSeries.subsingleton_iff
{R : Type u_1}
[Semiring R]
:
Subsingleton (PowerSeries R) ↔ Subsingleton R
theorem
PowerSeries.coeff_X
{R : Type u_1}
[Semiring R]
(n : ℕ)
:
(PowerSeries.coeff R n) PowerSeries.X = if n = 1 then 1 else 0
@[simp]
theorem
PowerSeries.coeff_zero_X
{R : Type u_1}
[Semiring R]
:
(PowerSeries.coeff R 0) PowerSeries.X = 0
@[simp]
theorem
PowerSeries.coeff_one_X
{R : Type u_1}
[Semiring R]
:
(PowerSeries.coeff R 1) PowerSeries.X = 1
@[simp]
theorem
PowerSeries.X_pow_eq
{R : Type u_1}
[Semiring R]
(n : ℕ)
:
PowerSeries.X ^ n = (PowerSeries.monomial R n) 1
theorem
PowerSeries.coeff_X_pow
{R : Type u_1}
[Semiring R]
(m : ℕ)
(n : ℕ)
:
(PowerSeries.coeff R m) (PowerSeries.X ^ n) = if m = n then 1 else 0
@[simp]
theorem
PowerSeries.coeff_X_pow_self
{R : Type u_1}
[Semiring R]
(n : ℕ)
:
(PowerSeries.coeff R n) (PowerSeries.X ^ n) = 1
@[simp]
theorem
PowerSeries.coeff_one
{R : Type u_1}
[Semiring R]
(n : ℕ)
:
(PowerSeries.coeff R n) 1 = if n = 0 then 1 else 0
theorem
PowerSeries.coeff_mul
{R : Type u_1}
[Semiring R]
(n : ℕ)
(φ : PowerSeries R)
(ψ : PowerSeries R)
:
(PowerSeries.coeff R n) (φ * ψ) = Finset.sum (Finset.antidiagonal n) fun (p : ℕ × ℕ) => (PowerSeries.coeff R p.1) φ * (PowerSeries.coeff R p.2) ψ
@[simp]
theorem
PowerSeries.coeff_mul_C
{R : Type u_1}
[Semiring R]
(n : ℕ)
(φ : PowerSeries R)
(a : R)
:
(PowerSeries.coeff R n) (φ * (PowerSeries.C R) a) = (PowerSeries.coeff R n) φ * a
@[simp]
theorem
PowerSeries.coeff_C_mul
{R : Type u_1}
[Semiring R]
(n : ℕ)
(φ : PowerSeries R)
(a : R)
:
(PowerSeries.coeff R n) ((PowerSeries.C R) a * φ) = a * (PowerSeries.coeff R n) φ
@[simp]
theorem
PowerSeries.coeff_smul
{R : Type u_1}
[Semiring R]
{S : Type u_2}
[Semiring S]
[Module R S]
(n : ℕ)
(φ : PowerSeries S)
(a : R)
:
(PowerSeries.coeff S n) (a • φ) = a • (PowerSeries.coeff S n) φ
theorem
PowerSeries.smul_eq_C_mul
{R : Type u_1}
[Semiring R]
(f : PowerSeries R)
(a : R)
:
a • f = (PowerSeries.C R) a * f
@[simp]
theorem
PowerSeries.coeff_succ_mul_X
{R : Type u_1}
[Semiring R]
(n : ℕ)
(φ : PowerSeries R)
:
(PowerSeries.coeff R (n + 1)) (φ * PowerSeries.X) = (PowerSeries.coeff R n) φ
@[simp]
theorem
PowerSeries.coeff_succ_X_mul
{R : Type u_1}
[Semiring R]
(n : ℕ)
(φ : PowerSeries R)
:
(PowerSeries.coeff R (n + 1)) (PowerSeries.X * φ) = (PowerSeries.coeff R n) φ
@[simp]
theorem
PowerSeries.constantCoeff_C
{R : Type u_1}
[Semiring R]
(a : R)
:
(PowerSeries.constantCoeff R) ((PowerSeries.C R) a) = a
@[simp]
theorem
PowerSeries.constantCoeff_zero
{R : Type u_1}
[Semiring R]
:
(PowerSeries.constantCoeff R) 0 = 0
theorem
PowerSeries.constantCoeff_one
{R : Type u_1}
[Semiring R]
:
(PowerSeries.constantCoeff R) 1 = 1
@[simp]
theorem
PowerSeries.constantCoeff_X
{R : Type u_1}
[Semiring R]
:
(PowerSeries.constantCoeff R) PowerSeries.X = 0
theorem
PowerSeries.coeff_zero_mul_X
{R : Type u_1}
[Semiring R]
(φ : PowerSeries R)
:
(PowerSeries.coeff R 0) (φ * PowerSeries.X) = 0
theorem
PowerSeries.coeff_zero_X_mul
{R : Type u_1}
[Semiring R]
(φ : PowerSeries R)
:
(PowerSeries.coeff R 0) (PowerSeries.X * φ) = 0
theorem
PowerSeries.coeff_C_mul_X_pow
{R : Type u_1}
[Semiring R]
(x : R)
(k : ℕ)
(n : ℕ)
:
(PowerSeries.coeff R n) ((PowerSeries.C R) x * PowerSeries.X ^ k) = if n = k then x else 0
@[simp]
theorem
PowerSeries.coeff_mul_X_pow
{R : Type u_1}
[Semiring R]
(p : PowerSeries R)
(n : ℕ)
(d : ℕ)
:
(PowerSeries.coeff R (d + n)) (p * PowerSeries.X ^ n) = (PowerSeries.coeff R d) p
@[simp]
theorem
PowerSeries.coeff_X_pow_mul
{R : Type u_1}
[Semiring R]
(p : PowerSeries R)
(n : ℕ)
(d : ℕ)
:
(PowerSeries.coeff R (d + n)) (PowerSeries.X ^ n * p) = (PowerSeries.coeff R d) p
theorem
PowerSeries.coeff_mul_X_pow'
{R : Type u_1}
[Semiring R]
(p : PowerSeries R)
(n : ℕ)
(d : ℕ)
:
(PowerSeries.coeff R d) (p * PowerSeries.X ^ n) = if n ≤ d then (PowerSeries.coeff R (d - n)) p else 0
theorem
PowerSeries.coeff_X_pow_mul'
{R : Type u_1}
[Semiring R]
(p : PowerSeries R)
(n : ℕ)
(d : ℕ)
:
(PowerSeries.coeff R d) (PowerSeries.X ^ n * p) = if n ≤ d then (PowerSeries.coeff R (d - n)) p else 0
theorem
PowerSeries.isUnit_constantCoeff
{R : Type u_1}
[Semiring R]
(φ : PowerSeries R)
(h : IsUnit φ)
:
IsUnit ((PowerSeries.constantCoeff R) φ)
If a formal power series is invertible, then so is its constant coefficient.
theorem
PowerSeries.eq_shift_mul_X_add_const
{R : Type u_1}
[Semiring R]
(φ : PowerSeries R)
:
φ = (PowerSeries.mk fun (p : ℕ) => (PowerSeries.coeff R (p + 1)) φ) * PowerSeries.X + (PowerSeries.C R) ((PowerSeries.constantCoeff R) φ)
Split off the constant coefficient.
theorem
PowerSeries.eq_X_mul_shift_add_const
{R : Type u_1}
[Semiring R]
(φ : PowerSeries R)
:
φ = (PowerSeries.X * PowerSeries.mk fun (p : ℕ) => (PowerSeries.coeff R (p + 1)) φ) + (PowerSeries.C R) ((PowerSeries.constantCoeff R) φ)
Split off the constant coefficient.
@[simp]
theorem
PowerSeries.map_comp
{R : Type u_1}
[Semiring R]
{S : Type u_2}
{T : Type u_3}
[Semiring S]
[Semiring T]
(f : R →+* S)
(g : S →+* T)
:
PowerSeries.map (RingHom.comp g f) = RingHom.comp (PowerSeries.map g) (PowerSeries.map f)
@[simp]
theorem
PowerSeries.coeff_map
{R : Type u_1}
[Semiring R]
{S : Type u_2}
[Semiring S]
(f : R →+* S)
(n : ℕ)
(φ : PowerSeries R)
:
(PowerSeries.coeff S n) ((PowerSeries.map f) φ) = f ((PowerSeries.coeff R n) φ)
@[simp]
theorem
PowerSeries.map_C
{R : Type u_1}
[Semiring R]
{S : Type u_2}
[Semiring S]
(f : R →+* S)
(r : R)
:
(PowerSeries.map f) ((PowerSeries.C R) r) = (PowerSeries.C S) (f r)
@[simp]
theorem
PowerSeries.map_X
{R : Type u_1}
[Semiring R]
{S : Type u_2}
[Semiring S]
(f : R →+* S)
:
(PowerSeries.map f) PowerSeries.X = PowerSeries.X
theorem
PowerSeries.X_pow_dvd_iff
{R : Type u_1}
[Semiring R]
{n : ℕ}
{φ : PowerSeries R}
:
PowerSeries.X ^ n ∣ φ ↔ ∀ m < n, (PowerSeries.coeff R m) φ = 0
theorem
PowerSeries.X_dvd_iff
{R : Type u_1}
[Semiring R]
{φ : PowerSeries R}
:
PowerSeries.X ∣ φ ↔ (PowerSeries.constantCoeff R) φ = 0
The ring homomorphism taking a power series f(X) to f(aX).
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
PowerSeries.coeff_rescale
{R : Type u_1}
[CommSemiring R]
(f : PowerSeries R)
(a : R)
(n : ℕ)
:
(PowerSeries.coeff R n) ((PowerSeries.rescale a) f) = a ^ n * (PowerSeries.coeff R n) f
@[simp]
theorem
PowerSeries.rescale_zero_apply
{R : Type u_1}
[CommSemiring R]
:
(PowerSeries.rescale 0) PowerSeries.X = (PowerSeries.C R) ((PowerSeries.constantCoeff R) PowerSeries.X)
@[simp]
theorem
PowerSeries.rescale_mk
{R : Type u_1}
[CommSemiring R]
(f : ℕ → R)
(a : R)
:
(PowerSeries.rescale a) (PowerSeries.mk f) = PowerSeries.mk fun (n : ℕ) => a ^ n * f n
theorem
PowerSeries.rescale_rescale
{R : Type u_1}
[CommSemiring R]
(f : PowerSeries R)
(a : R)
(b : R)
:
(PowerSeries.rescale b) ((PowerSeries.rescale a) f) = (PowerSeries.rescale (a * b)) f
theorem
PowerSeries.rescale_mul
{R : Type u_1}
[CommSemiring R]
(a : R)
(b : R)
:
PowerSeries.rescale (a * b) = RingHom.comp (PowerSeries.rescale b) (PowerSeries.rescale a)
theorem
PowerSeries.coeff_prod
{R : Type u_2}
[CommSemiring R]
{ι : Type u_3}
[DecidableEq ι]
(f : ι → PowerSeries R)
(d : ℕ)
(s : Finset ι)
:
(PowerSeries.coeff R d) (Finset.prod s fun (j : ι) => f j) = Finset.sum (Finset.piAntidiagonal s d) fun (l : ι →₀ ℕ) =>
Finset.prod s fun (i : ι) => (PowerSeries.coeff R (l i)) (f i)
Coefficients of a product of power series
@[simp]
theorem
PowerSeries.rescale_X
{A : Type u_2}
[CommRing A]
(a : A)
:
(PowerSeries.rescale a) PowerSeries.X = (PowerSeries.C A) a * PowerSeries.X
theorem
PowerSeries.rescale_neg_one_X
{A : Type u_2}
[CommRing A]
:
(PowerSeries.rescale (-1)) PowerSeries.X = -PowerSeries.X
The ring homomorphism taking a power series f(X) to f(-X).
Equations
- PowerSeries.evalNegHom = PowerSeries.rescale (-1)
Instances For
theorem
PowerSeries.eq_zero_or_eq_zero_of_mul_eq_zero
{R : Type u_1}
[Ring R]
[NoZeroDivisors R]
(φ : PowerSeries R)
(ψ : PowerSeries R)
(h : φ * ψ = 0)
:
instance
PowerSeries.instIsDomainPowerSeriesInstSemiringPowerSeriesToSemiring
{R : Type u_1}
[Ring R]
[IsDomain R]
:
IsDomain (PowerSeries R)
Equations
- ⋯ = ⋯
theorem
PowerSeries.span_X_isPrime
{R : Type u_1}
[CommRing R]
[IsDomain R]
:
Ideal.IsPrime (Ideal.span {PowerSeries.X})
The ideal spanned by the variable in the power series ring over an integral domain is a prime ideal.
theorem
PowerSeries.X_irreducible
{R : Type u_1}
[CommRing R]
[IsDomain R]
:
Irreducible PowerSeries.X
The variable of the power series ring over an integral domain is irreducible.
theorem
PowerSeries.rescale_injective
{R : Type u_1}
[CommRing R]
[IsDomain R]
{a : R}
(ha : a ≠ 0)
:
theorem
PowerSeries.C_eq_algebraMap
{R : Type u_1}
[CommSemiring R]
{r : R}
:
(PowerSeries.C R) r = (algebraMap R (PowerSeries R)) r
theorem
PowerSeries.algebraMap_apply
{R : Type u_1}
{A : Type u_2}
[CommSemiring R]
[Semiring A]
[Algebra R A]
{r : R}
:
(algebraMap R (PowerSeries A)) r = (PowerSeries.C A) ((algebraMap R A) r)
instance
PowerSeries.instNontrivialSubalgebraPowerSeriesInstSemiringPowerSeriesToSemiringInstAlgebraPowerSeriesInstSemiringPowerSeriesId
{R : Type u_1}
[CommSemiring R]
[Nontrivial R]
:
Nontrivial (Subalgebra R (PowerSeries R))
Equations
- ⋯ = ⋯
The natural inclusion from polynomials into formal power series.
Equations
- ↑φ = PowerSeries.mk fun (n : ℕ) => Polynomial.coeff φ n
Instances For
instance
Polynomial.coeToPowerSeries
{R : Type u_2}
[CommSemiring 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_2}
[CommSemiring R]
(φ : Polynomial R)
:
↑φ = PowerSeries.mk (Polynomial.coeff φ)
@[simp]
theorem
Polynomial.coeff_coe
{R : Type u_2}
[CommSemiring R]
(φ : Polynomial R)
(n : ℕ)
:
(PowerSeries.coeff R n) ↑φ = Polynomial.coeff φ n
@[simp]
theorem
Polynomial.coe_monomial
{R : Type u_2}
[CommSemiring R]
(n : ℕ)
(a : R)
:
↑((Polynomial.monomial n) a) = (PowerSeries.monomial R n) a
@[simp]
@[simp]
@[simp]
theorem
Polynomial.coe_C
{R : Type u_2}
[CommSemiring R]
(a : R)
:
↑(Polynomial.C a) = (PowerSeries.C R) a
@[simp]
@[simp]
@[simp]
@[simp]
theorem
Polynomial.constantCoeff_coe
{R : Type u_2}
[CommSemiring R]
(φ : Polynomial R)
:
(PowerSeries.constantCoeff R) ↑φ = Polynomial.coeff φ 0
@[simp]
@[simp]
@[simp]
def
Polynomial.coeToPowerSeries.ringHom
{R : Type u_2}
[CommSemiring R]
:
Polynomial R →+* PowerSeries R
The coercion from polynomials to power series as a ring homomorphism.
Equations
- Polynomial.coeToPowerSeries.ringHom = { toMonoidHom := { toOneHom := { toFun := Coe.coe, map_one' := ⋯ }, map_mul' := ⋯ }, map_zero' := ⋯, map_add' := ⋯ }
Instances For
@[simp]
theorem
Polynomial.coeToPowerSeries.ringHom_apply
{R : Type u_2}
[CommSemiring R]
(φ : Polynomial R)
:
Polynomial.coeToPowerSeries.ringHom φ = ↑φ
@[simp]
theorem
Polynomial.eval₂_C_X_eq_coe
{R : Type u_2}
[CommSemiring R]
(φ : Polynomial R)
:
Polynomial.eval₂ (PowerSeries.C R) PowerSeries.X φ = ↑φ
def
Polynomial.coeToPowerSeries.algHom
{R : Type u_2}
[CommSemiring R]
(A : Type u_3)
[Semiring A]
[Algebra R A]
:
Polynomial R →ₐ[R] PowerSeries A
The coercion from polynomials to power series as an algebra homomorphism.
Equations
- Polynomial.coeToPowerSeries.algHom A = let __src := RingHom.comp (PowerSeries.map (algebraMap R A)) Polynomial.coeToPowerSeries.ringHom; { toRingHom := __src, commutes' := ⋯ }
Instances For
@[simp]
theorem
Polynomial.coeToPowerSeries.algHom_apply
{R : Type u_2}
[CommSemiring R]
(φ : Polynomial R)
(A : Type u_3)
[Semiring A]
[Algebra R A]
:
(Polynomial.coeToPowerSeries.algHom A) φ = (PowerSeries.map (algebraMap R A)) ↑φ
instance
PowerSeries.algebraPolynomial
{R : Type u_1}
{A : Type u_2}
[CommSemiring R]
[CommSemiring A]
[Algebra R A]
:
Algebra (Polynomial R) (PowerSeries A)
Equations
- PowerSeries.algebraPolynomial = RingHom.toAlgebra (Polynomial.coeToPowerSeries.algHom A).toRingHom
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 = RingHom.toAlgebra (PowerSeries.map (algebraMap R A))
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' = RingHom.toAlgebra (RingHom.comp Polynomial.coeToPowerSeries.ringHom (algebraMap R (Polynomial A)))
theorem
PowerSeries.algebraMap_apply'
{R : Type u_1}
(A : Type u_2)
[CommSemiring R]
[CommSemiring A]
[Algebra R A]
(p : Polynomial R)
:
(algebraMap (Polynomial R) (PowerSeries A)) p = (PowerSeries.map (algebraMap R A)) ↑p
theorem
PowerSeries.algebraMap_apply''
{R : Type u_1}
(A : Type u_2)
[CommSemiring R]
[CommSemiring A]
[Algebra R A]
(f : PowerSeries R)
:
(algebraMap (PowerSeries R) (PowerSeries A)) f = (PowerSeries.map (algebraMap R A)) f