---

Step * of Lemma fps-scalar-mul-slice

∀[X:Type]. ∀[r:CRng]. ∀[c:|r|]. ∀[n:ℤ]. ∀[g:PowerSeries(X;r)].  ([(c)*g]_n = (c)*[g]_n ∈ PowerSeries(X;r))
BY
{ (Auto
   THEN BLemma `fps-ext`
   THEN Auto
   THEN (RepUR ``fps-slice fps-scalar-mul fps-coeff`` 0 THEN AutoSplit THEN RW RngNormC 0 THEN Auto)⋅) }

---

Latex:

---

Latex:
\mforall{}[X:Type].  \mforall{}[r:CRng].  \mforall{}[c:|r|].  \mforall{}[n:\mBbbZ{}].  \mforall{}[g:PowerSeries(X;r)].    ([(c)*g]\_n  =  (c)*[g]\_n)


By

---

Latex:
(Auto
  THEN  BLemma  `fps-ext`
  THEN  Auto
  THEN  (RepUR  ``fps-slice  fps-scalar-mul  fps-coeff``  0  THEN  AutoSplit  THEN  RW  RngNormC  0  THEN  Auto)\mcdot{})

---

Home Index