English
If S is a semiring and R an ambient ring acting on Laurent series over S, then scaling a Laurent series by r∈R before embedding into power series is the same as embedding first and then scaling by r.
Русский
Если S — полурёд, а R — полукольцо, действующее на лорентовские ряды над S, то умножение ряда на скаляр r сначала в R, затем в структуре степенного ряда над S, эквивалентно встраиванию в проницаемую структуру и последующему умножению на r.
LaTeX
$$$\forall r\in R,\; \forall x\in S\langle\!X\!\rangle,\; ((r\cdot x):S\langle\!X\!\rangle) = r\cdot (\mathrm{ofPowerSeries}\,\mathbb{Z}\,S\,x).$$$
Lean4
@[simp, norm_cast]
theorem coe_smul {S : Type*} [Semiring S] [Module R S] (r : R) (x : S⟦X⟧) :
((r • x : S⟦X⟧) : S⸨X⸩) = r • (ofPowerSeries ℤ S x) :=
by
ext
simp [coeff_coe, coeff_smul, smul_ite]
