Step
*
of Lemma
mul_over_plus_fps
No Annotations
∀[X:Type]
∀[eq:EqDecider(X)]. ∀[r:CRng]. ∀[a,b,c:PowerSeries(X;r)].
(((a*(b+c)) = ((a*b)+(a*c)) ∈ PowerSeries(X;r)) ∧ (((b+c)*a) = ((b*a)+(c*a)) ∈ PowerSeries(X;r)))
supposing valueall-type(X)
BY
{ (RepeatFor 3 ((D 0 THENA Auto))
THEN (ProveSpecializedLemmaWReduce rng_times_over_plus) 1 [⌜parm{i}⌝;⌜⌜fps-rng(r)⌝⌝]⋅
) }
Latex:
Latex:
No Annotations
\mforall{}[X:Type]
\mforall{}[eq:EqDecider(X)]. \mforall{}[r:CRng]. \mforall{}[a,b,c:PowerSeries(X;r)].
(((a*(b+c)) = ((a*b)+(a*c))) \mwedge{} (((b+c)*a) = ((b*a)+(c*a))))
supposing valueall-type(X)
By
Latex:
(RepeatFor 3 ((D 0 THENA Auto))
THEN (ProveSpecializedLemmaWReduce rng\_times\_over\_plus) 1 [\mkleeneopen{}parm\{i\}\mkleeneclose{};\mkleeneopen{}\mkleeneopen{}fps-rng(r)\mkleeneclose{}\mkleeneclose{}]\mcdot{}
)
Home
Index