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