Def  P & Q == PQ

is mentioned by

Thm*  n:{1...}.  Thm*  h:({2..(n+1)}).  Thm*  n = {2..n+1}(h) & is_prime_factorization(2; (n+1); h)	[prime_factorization_exists]
Thm*  k:{2...}, n:, g:({2..k}). Thm*  2  n < k+1 Thm*   Thm*  (i:{2..k}. ni  0<g(i)  prime(i)) Thm*   Thm*  (h:({2..k}).  Thm*  ({2..k}(g) = {2..k}(h) & is_prime_factorization(2; k; h))	[prime_factorization_existsLEMMA]
Thm*  k:{2...}, g:({2..k}), z:{2..k}. Thm*  prime(z) Thm*   Thm*  (g':({2..k}).  Thm*  ({2..k}(g) = {2..k}(g') Thm*  (& g'(z) = 0 Thm*  (& (u:{2..k}. z<u  g'(u) = g(u)))	[can_reduce_composite_factor2]
Thm*  k:{2...}, g:({2..k}), x,y:{2..k}. Thm*  xy<k Thm*   Thm*  (h:({2..k}).  Thm*  ({2..k}(g) = {2..k}(h) Thm*  (& h(xy) = 0 Thm*  (& (u:{2..k}. xy<u  h(u) = g(u)))	[can_reduce_composite_factor]
Thm*  k:{2...}, g:({2..k}), x:{2..k}. Thm*  xx<k Thm*   Thm*  {2..k}(g) = {2..k}(split_factor1(g; x)) Thm*  & split_factor1(g; x)(xx) = 0 Thm*  & (u:{2..k}. xx<u  split_factor1(g; x)(u) = g(u))	[split_factor1_char]
Thm*  k:{2...}, g:({2..k}), x,y:{2..k}. Thm*  xy<k Thm*   Thm*  x<y Thm*   Thm*  {2..k}(g) = {2..k}(split_factor2(g; x; y)) Thm*  & split_factor2(g; x; y)(xy) = 0 Thm*  & (u:{2..k}. xy<u  split_factor2(g; x; y)(u) = g(u))	[split_factor2_char]
Thm*  p:. prime(p)  (b,z:. p | zb  b  0 & p | z)	[prime_divs_exp]
Def  f is a factorization of k Def  == (x:Prime. k<x  f(x) = 0) & k = {2..k+1}(prime_mset_complete(f))	[prime_factorization_of]

In prior sections: core int 1 bool 1 LogicSupplement int 2 num thy 1 SimpleMulFacts IteratedBinops rel 1

Try larger context: DiscrMathExt IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html