---

Step * of Lemma fps-neg-slice

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

---

Latex:

---

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


By

---

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

---

Home Index