a,b:
, f,g:({a..b
}
).
Thm*
{a..b}(f)
{a..b}(g) = {a..b}(
i.f(i)+g(i))a,b:, f,g:({a..b}).
Thm* (
i:{a..b}. f(i))( i:{a..b}. g(i)) = ( i:{a..b}. f(i)g(i))i:, x,y:. ixiy = i(x+y)| Rank | Theorem | Name |
| 5 | a,b:, f,g:({a..b}).
Thm* {a..b}(f){a..b}(g) = {a..b}(i.f(i)+g(i)) | [eval_factorization_prod] |
| cites the following: | ||
| 3 | a,b:, f,g:({a..b}).
Thm* ( i:{a..b}. f(i))( i:{a..b}. g(i)) = ( i:{a..b}. f(i)g(i)) | [mul_via_intseg_factors] |
| 4 | i:, x,y:. ixiy = i(x+y) | [sum_exponent] |