a,b:
, f:({a..b
}
), z:{a..b}.
Thm* 0<f(z)
{a..b}(f) = z
{a..b}(reduce_factorization(f; z))a,b:, j:{a..b}. {a..b}(trivial_factorization(j)) = ja,b:, f,g:({a..b}).
Thm*
{a..b}(f){a..b}(g) = {a..b}(
i.f(i)+g(i))| Rank | Theorem | Name |
| 6 | a,b:, f:({a..b}), z:{a..b}.
Thm* 0<f(z) {a..b}(f) = z{a..b}(reduce_factorization(f; z)) | [eval_factorization_pluck] |
| cites the following: | ||
| 5 | a,b:, j:{a..b}. {a..b}(trivial_factorization(j)) = j | [eval_trivial_factorization] |
| 5 | a,b:, f,g:({a..b}).
Thm* {a..b}(f){a..b}(g) = {a..b}(i.f(i)+g(i)) | [eval_factorization_prod] |