is mentioned by
![]() Thm* ![]() ![]() ![]() ![]() ![]() Thm* n = ![]() ![]() ![]() | [prime_factorization_exists] |
![]() ![]() ![]() ![]() ![]() ![]() Thm* 2 ![]() Thm* ![]() ![]() Thm* ( ![]() ![]() ![]() ![]() ![]() ![]() ![]() Thm* ![]() ![]() Thm* ( ![]() ![]() ![]() ![]() ![]() Thm* ( ![]() ![]() ![]() ![]() ![]() ![]() | [prime_factorization_existsLEMMA] |
![]() ![]() ![]() ![]() ![]() ![]() Thm* is_prime_factorization(a; b; g) Thm* ![]() ![]() Thm* is_prime_factorization(a; b; h) ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | [prime_factorization_unique] |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() Thm* is_prime_factorization(a; b; f) Thm* ![]() ![]() Thm* prime(p) Thm* ![]() ![]() Thm* p | ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | [remove_prime_factor] |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() Thm* is_prime_factorization(a; b; f) Thm* ![]() ![]() Thm* prime(p) ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | [prime_factorization_includes_prime_divisors] |
![]() ![]() ![]() ![]() ![]() ![]() ![]() Thm* 0<f(j) Thm* ![]() ![]() Thm* is_prime_factorization(a; b; f) Thm* ![]() ![]() Thm* is_prime_factorization(a; b; reduce_factorization(f; j)) | [reduce_fac_pres_isprimefac] |
![]() ![]() ![]() ![]() ![]() ![]() | [sq_stable__is_prime_factorization] |
![]() ![]() ![]() ![]() ![]() ![]() | [prime_mset_c_is_prime_f] |
Try larger context:
DiscrMathExt
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html