English
For a polynomial f in one unit variable, its power-series image equals the power-series image of f under the pUnitAlgEquiv. In other words, a natural identification between univariate mv-polynomials and power series respects the pUnit structure.
Русский
Для много переменных полиномов в единичной переменной их изображение как ряд степенных совпадает с изображением через pUnitAlgEquiv; естественное соответствие сохраняет структуру единицы.
LaTeX
$$$(f.toMvPowerSeries : \\mathrm{PowerSeries}(R)) = (f.pUnitAlgEquiv(R)).toPowerSeries$$$
Lean4
theorem _root_.MvPolynomial.toMvPowerSeries_pUnitAlgEquiv {f : MvPolynomial PUnit R} :
(f.toMvPowerSeries : PowerSeries R) = (f.pUnitAlgEquiv R).toPowerSeries := by
induction f using MvPolynomial.induction_on' with
| monomial d r =>
--Note: this `have` should be a generic `simp` lemma for a `Unique` type with `()` replaced
--by any element.
have : single () (d ()) = d := by ext; simp
simp only [MvPolynomial.coe_monomial, MvPolynomial.pUnitAlgEquiv_monomial, Polynomial.coe_monomial,
PowerSeries.monomial, this]
| add f g hf hg => simp [hf, hg]
