English
The symmetry of the pUnit algebra equivalence preserves the power-series realization; applying the inverse pUnitAlgEquiv and then converting to a mv-power-series matches taking the power-series image first and then applying the inverse equivalence.
Русский
Симметрия эквивалентности pUnit сохраняет реализацию в виде ряда степенных; применение обратной эквивалентности и затем переход к mv-ряду совпадают с сначала получением ряда степенных, затем применением обратной эквивалентности.
LaTeX
$$$((f.toPowerSeries) : \\mathrm{MvPowerSeries} PUnit R) = ((\\mathrm{pUnitAlgEquiv}(R)).symm f).toMvPowerSeries$$$
Lean4
theorem pUnitAlgEquiv_symm_toPowerSeries {f : Polynomial R} :
((f.toPowerSeries) : MvPowerSeries PUnit R) = ((MvPolynomial.pUnitAlgEquiv R).symm f).toMvPowerSeries :=
by
set g := (MvPolynomial.pUnitAlgEquiv R).symm f
have : f = MvPolynomial.pUnitAlgEquiv R g := by simp only [g, AlgEquiv.apply_symm_apply]
rw [this, MvPolynomial.toMvPowerSeries_pUnitAlgEquiv]
