Rank | Theorem | Name |
20 | Thm* is_prime_factorization(a; b; f) Thm* Thm* prime(p) Thm* Thm* p | {a..b}(f) {a..b}(f) = p{a..b}(reduce_factorization(f; p)) | [remove_prime_factor] |
cites the following: | ||
19 | Thm* is_prime_factorization(a; b; f) Thm* Thm* prime(p) p | {a..b}(f) p {a..b} & 0<f(p) | [prime_factorization_includes_prime_divisors] |
6 | Thm* 0<f(z) {a..b}(f) = z{a..b}(reduce_factorization(f; z)) | [eval_factorization_pluck] |