a,b:
, f:({a..b
}
), j:{a..b}. 0<f(j) 
j | 
{a..b}(f)a,b:, f:({a..b}), z:{a..b}.
Thm* 0<f(z)
{a..b}(f) = z
{a..b}(reduce_factorization(f; z))| Rank | Theorem | Name |
| 7 | a,b:, f:({a..b}), j:{a..b}. 0<f(j) j | {a..b}(f) | [factor_divides_evalfactorization] |
| cites the following: | ||
| 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] |