---

Step * 1 of Lemma fps-scalar-mul-property


1. X : Type
2. valueall-type(X)
3. eq : EqDecider(X)
4. r : CRng
5. Comm(|r|;+r)
6. Assoc(|r|;+r)
7. BiLinear(|r|;+r;*) ∧ IsMonoid(|r|;+r;0) ∧ (∃minus:|r| ⟶ |r|. IsGroup(|r|;+r;0;minus))
⊢ (IsAction(|r|;*;1;PowerSeries(X;r);λc,f. (c)*f)
∧ IsBilinear(|r|;PowerSeries(X;r);PowerSeries(X;r);+r;λf,g. (f+g);λf,g. (f+g);λc,f. (c)*f))
∧ (∀c:|r|. Dist1op2opLR(PowerSeries(X;r);λf.(c)*f;λf,g. (f*g)))
BY
{ xxx(Auto
      THEN D 0
      THEN (Reduce 0 THEN Auto)
      THEN (BLemma `fps-ext` THEN Auto)
      THEN Try ((RepUR ``fps-scalar-mul fps-add fps-mul fps-coeff`` 0
                 THEN RW CRngNormC 0
                 THEN Auto
                 THEN Try ((Unfold `infix_ap` 0 THEN Complete (Auto))))⋅)
      THEN (RWO "bag-summation-linear1-right<" 0
            THEN Auto
            THEN Try ((BLemma `bag-summation-equal` THEN Auto))
            THEN Try ((RW CRngNormC 0 THEN Auto THEN Unfold `infix_ap` 0 THEN Auto)))⋅)⋅xxx }

---

Latex:

---

Latex:

1.  X  :  Type
2.  valueall-type(X)
3.  eq  :  EqDecider(X)
4.  r  :  CRng
5.  Comm(|r|;+r)
6.  Assoc(|r|;+r)
7.  BiLinear(|r|;+r;*)  \mwedge{}  IsMonoid(|r|;+r;0)  \mwedge{}  (\mexists{}minus:|r|  {}\mrightarrow{}  |r|.  IsGroup(|r|;+r;0;minus))
\mvdash{}  (IsAction(|r|;*;1;PowerSeries(X;r);\mlambda{}c,f.  (c)*f)
\mwedge{}  IsBilinear(|r|;PowerSeries(X;r);PowerSeries(X;r);+r;\mlambda{}f,g.  (f+g);\mlambda{}f,g.  (f+g);\mlambda{}c,f.  (c)*f))
\mwedge{}  (\mforall{}c:|r|.  Dist1op2opLR(PowerSeries(X;r);\mlambda{}f.(c)*f;\mlambda{}f,g.  (f*g)))


By

---

Latex:
xxx(Auto
        THEN  D  0
        THEN  (Reduce  0  THEN  Auto)
        THEN  (BLemma  `fps-ext`  THEN  Auto)
        THEN  Try  ((RepUR  ``fps-scalar-mul  fps-add  fps-mul  fps-coeff``  0
                              THEN  RW  CRngNormC  0
                              THEN  Auto
                              THEN  Try  ((Unfold  `infix\_ap`  0  THEN  Complete  (Auto))))\mcdot{})
        THEN  (RWO  "bag-summation-linear1-right<"  0
                    THEN  Auto
                    THEN  Try  ((BLemma  `bag-summation-equal`  THEN  Auto))
                    THEN  Try  ((RW  CRngNormC  0  THEN  Auto  THEN  Unfold  `infix\_ap`  0  THEN  Auto)))\mcdot{})\mcdot{}xxx

---

Home Index