Theorems · Definition · commutative algebra

PowerSeries.toMvPowerSeries

{R : Type u_1} → {σ : Type u_2} → [inst : CommSemiring R] → σ → PowerSeries R →ₐ[R] MvPowerSeries σ R

Given a power series p : R⟦X⟧ and an index i, we may view it as a multivariate power series toMvPowerSeries i p : MvPowerSeries σ R.

Defined in

Mathlib.RingTheory.MvPowerSeries.Equiv

Cited by

11 results in Mathlib

Foundations

Depth 100 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommSemiring