THM | extend_intseg_upperpart_down
|
![]() ![]() ![]() ![]() ![]() ![]() P(n-1) ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
def | prime_mset_complete
|
![]() |
THM | prime_mset_complete_isext
|
![]() ![]() ![]() ![]() ![]() ![]() |
THM | prime_mset_complete_ismin
|
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
def | eval_factorization
|
The number of which an integer multiset is a factorization
![]() ![]() ![]() ![]() ![]() ![]() |
THM | eval_factorization_split_mid
|
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
def | prime_factorization_of
|
== ( ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
THM | prime_factorization_limit
|
![]() ![]() ![]() ![]() ![]() ![]() f is a factorization of n ![]() ![]() g is a factorization of n ![]() ![]() ( ![]() ![]() ![]() ![]() |
THM | eval_factorization_split_pluck
|
![]() ![]() ![]() ![]() ![]() ![]() a ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
def | trivial_factorization
|
![]() ![]() |
THM | trivial_factorization_comp1
|
![]() ![]() ![]() ![]() ![]() ![]() |
THM | trivial_factorization_comp2
|
![]() ![]() ![]() ![]() ![]() ![]() ![]() |
THM | eval_trivial_factorization
|
![]() ![]() ![]() ![]() ![]() ![]() |
def | reduce_factorization
|
Removing one member from a factorization multiset
![]() ![]() |
THM | reduce_factorization_cancel
|
![]() ![]() ![]() ![]() ![]() ![]() ![]() 0<f(j) ![]() ![]() 0<g(j) ![]() ![]() ![]() ![]() |
THM | reduce_factorization_bound
|
![]() ![]() ![]() ![]() ![]() ![]() ![]() 0<f(j) ![]() ![]() ![]() ![]() ![]() |
THM | eval_factorization_nat_plus
|
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
THM | only_positives_prime_fed
|
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
THM | eval_factorization_one
|
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
THM | only_one_factored_by
|
![]() ![]() ![]() ![]() ![]() ![]() f is a factorization of n ![]() ![]() ![]() ![]() |
THM | eval_factorization_one_b
|
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
THM | eval_factorization_one_c
|
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
THM | eval_factorization_not_one
|
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
THM | eval_factorization_prod
|
The pairwise sum of factorizations of a couple of numbers factorizes their product.
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
THM | eval_factorization_pluck
|
![]() ![]() ![]() ![]() ![]() ![]() ![]() 0<f(z) ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
THM | eval_reduce_factorization_less
|
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() 2 ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
THM | eval_factorization_intseg_null
|
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
THM | eval_factorization_nullnorm
|
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
def | is_prime_factorization
|
Prime factorization as a multiset on an interval.
![]() ![]() ![]() ![]() |
THM | prime_mset_c_is_prime_f
|
![]() ![]() ![]() ![]() ![]() ![]() |
THM | sq_stable__is_prime_factorization
|
![]() ![]() ![]() ![]() ![]() ![]() |
THM | reduce_fac_pres_isprimefac
|
![]() ![]() ![]() ![]() ![]() ![]() ![]() 0<f(j) ![]() ![]() is_prime_factorization(a; b; f) ![]() ![]() is_prime_factorization(a; b; reduce_factorization(f; j)) |
THM | factor_divides_evalfactorization
|
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
THM | nat_prime_div_each_factorLEMMA
|
![]() ![]() prime(X) ![]() ![]() ( ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ( ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
THM | nat_prime_div_each_factor
|
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
THM | prime_divs_mul_via_intseg
|
![]() ![]() prime(p) ![]() ![]() ( ![]() ![]() ![]() ![]() ![]() ![]() (a<b ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
THM | prime_divs_exp
|
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
THM | prime_factorization_includes_prime_divisors
|
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() is_prime_factorization(a; b; f) ![]() ![]() prime(p) ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
THM | remove_prime_factor
|
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() is_prime_factorization(a; b; f) ![]() ![]() prime(p) ![]() ![]() p | ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
THM | prime_factorization_unique
|
There is at most one prime factorization of any natural number (given a range of integers to include).
![]() ![]() ![]() ![]() ![]() ![]() is_prime_factorization(a; b; g) ![]() ![]() is_prime_factorization(a; b; h) ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
def | split_factor2
|
(eliminating the power of a composite of two number by adding it to the power of its two factors)
== if u= ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
THM | split_factor2_char
|
Redistributing the power of a composite of two numbers in a factorization down to the factors produces another factorization of the same number, zeroing the power of the composite and leaving the powers of larger factors untouched.
![]() ![]() ![]() ![]() ![]() ![]() x ![]() ![]() ![]() x<y ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() & split_factor2(g; x; y)(x ![]() & ( ![]() ![]() ![]() ![]() ![]() |
def | split_factor1
|
![]() ![]() ![]() ![]() ![]() ![]() ![]() |
THM | split_factor1_char
|
Redistributing the power of a composite square in a factorization down to the square root produces another factorization of the same number, zeroing the power of the composite and leaving the powers of larger factors untouched.
![]() ![]() ![]() ![]() ![]() ![]() x ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() & split_factor1(g; x)(x ![]() & ( ![]() ![]() ![]() ![]() ![]() |
THM | can_reduce_composite_factor
|
A composite factor in a factorization can be reduced to power zero, leaving all larger factors' powers unchanged.
![]() ![]() ![]() ![]() ![]() ![]() x ![]() ![]() ![]() ( ![]() ![]() ![]() ![]() ![]() ( ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
THM | can_reduce_composite_factor2
|
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ( ![]() ![]() ![]() ![]() ![]() ( ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
THM | prime_factorization_existsLEMMA
|
![]() ![]() ![]() ![]() ![]() ![]() 2 ![]() ![]() ![]() ( ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ( ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
THM | prime_factorization_exists
|
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
def | lelt_int
|
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
THM | lelt_int_vs_lelt
|
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
def | complete_intseg_mset
|
![]() ![]() ![]() ![]() |
THM | complete_intseg_mset_ismin
|
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
THM | complete_intseg_mset_isext
|
![]() ![]() ![]() ![]() ![]() ![]() ![]() |
THM | prime_factorization_exists2
|
Every positive integer can be factored into primes.
![]() ![]() ![]() ![]() ![]() ![]() |
THM | prime_factorization_mset_unique
|
There is at most one prime factorization of any natural number.
![]() ![]() ![]() ![]() ![]() ![]() f is a factorization of n ![]() ![]() ![]() ![]() |
THM | fta_mset
|
The Fundamental Theorem of Arithmetic (FTA)
There is a unique prime factorization for every positive integer. ![]() ![]() ![]() ![]() ![]() ![]() |