Coefficients of a one-variable power series viewed in one variable of a family

PowerSeries.toMvPowerSeries i views a one-variable power series as a multivariate one in the single variable i. Mathlib records that it is an algebra map, how it acts on C and X, that it is injective, and that its coefficients vanish off the powers of i (PowerSeries.toMvPowerSeries_coeff_eq_zero); this file adds the remaining half, the value of the coefficients that do not vanish.

Main results

• PowerSeries.coeff_toMvPowerSeries: the coefficients of w.toMvPowerSeries i.

Provenance

Adapted from Michael Stoll's EllipticCurves project (github.com/MichaelStollBayreuth/EllipticCurves, Apache-2.0, pinned by TauCetiRoadmap/EllipticCurves/README.md at 66889eada51a), EllipticCurves/WeierstrassFormalGroup/Chord.lean, the private lemma coeff_rename_single. There it is stated for MvPowerSeries.rename (fun _ => s) and only where it is used; here it is stated for the PowerSeries.toMvPowerSeries spelling of that map, which is Mathlib's, and it carries no elliptic content so it is recorded on its own.

@[simp]

theorem PowerSeries.coeff_toMvPowerSeries {σ : Type u_1} {R : Type u_2} [CommSemiring R] [DecidableEq σ] (i : σ) (w : PowerSeries R) (d : σ →₀ ℕ) : (MvPowerSeries.coeff d) ((toMvPowerSeries i) w) = if d = Finsupp.single i (d i) then (coeff (d i)) w else 0

The coefficients of a one-variable power series viewed in the single variable i: the coefficient of a monomial d is the d i-th coefficient of the original series if d is a power of i, and 0 otherwise.

@[simp]

theorem PowerSeries.map_toMvPowerSeries {σ : Type u_1} {R : Type u_2} [CommSemiring R] {S : Type u_3} [CommSemiring S] (φ : R →+* S) (i : σ) (w : PowerSeries R) : (MvPowerSeries.map φ) ((toMvPowerSeries i) w) = (toMvPowerSeries i) ((map φ) w)

Base change commutes with viewing a one-variable series in a single variable i.