f:(Prime
), b:. is_prime_factorization(2; b; prime_mset_complete(f))f:(Prime), x:. 
prime(x) 
prime_mset_complete(f)(x) = 0| Theorem | Name |
| f:(Prime), b:. is_prime_factorization(2; b; prime_mset_complete(f)) | [prime_mset_c_is_prime_f] |
| cites the following: | |
| f:(Prime), x:. prime(x) prime_mset_complete(f)(x) = 0 | [prime_mset_complete_ismin] |