Description: The coefficient vector of multiplication in the univariate power series ring. (Contributed by Stefan O'Rear, 25-Mar-2015)
Ref | Expression | ||
---|---|---|---|
Hypotheses | coe1mul2.s | |
|
coe1mul2.t | |
||
coe1mul2.u | |
||
coe1mul2.b | |
||
Assertion | coe1mul2 | |