| Who Cites is prime factorization? |
|
is_prime_factorization | Def is_prime_factorization(a; b; f) == i:{a..b }. 0<f(i)  prime(i) |
| | Thm* a,b: , f:({a..b }  ). is_prime_factorization(a; b; f) Prop |
|
prime | Def prime(a) == a = 0 & (a ~ 1) & ( b,c: . a | b c  a | b a | c) |
| | Thm* a: . prime(a) Prop |
|
int_seg | Def {i..j } == {k: | i k < j } |
| | Thm* m,n: . {m..n } Type |
|
assoced | Def a ~ b == a | b & b | a |
| | Thm* a,b: . (a ~ b) Prop |
|
divides | Def b | a == c: . a = b c |
| | Thm* a,b: . (a | b) Prop |
|
lelt | Def i j < k == i j & j<k |
|
le | Def A B == B<A |
| | Thm* i,j: . (i j) Prop |
|
not | Def A == A  False |
| | Thm* A:Prop. ( A) Prop |