f:(Prime
), n:. f is a factorization of n 
0<na:
, b:
, f:({a..b
}). 
{a..b}(f) 
| Rank | Theorem | Name |
| 5 | f:(Prime), n:. f is a factorization of n 0<n | [only_positives_prime_fed] |
| cites the following: | ||
| 4 | a:, b:, f:({a..b}). {a..b}(f) | [eval_factorization_nat_plus] |