| i
j }
n:. {n...} 
TypeDef == (
x:Prime
. k<x 
f(x) = 0) & k = 
{2..k+1
}(prime_mset_complete(f))f:(Prime
), k:. f is a factorization of k Prop == {x:| prime(x) } == {i:| 0i } Type| Some definitions of interest. | |
| int_upper | | ij } |
| n:. {n...} Type | |
| prime_factorization_of | Def == ( x:Prime. k<x f(x) = 0) & k = {2..k+1}(prime_mset_complete(f)) |
| f:(Prime), k:. f is a factorization of k Prop | |
| prime_nats | == {x:| prime(x) } |
| nat | == {i:| 0i } |
| Type |
About:
 |  |  |  |  |  |  |  |
 |  |  |  |  |  |  |