Def  prime_mset_complete(f)(x) == if is_prime(x) f(x) else 0 fi

is mentioned by

Thm*  f:(Prime), b:. is_prime_factorization(2; b; prime_mset_complete(f))	[prime_mset_c_is_prime_f]
Thm*  n:, f,g:(Prime). Thm*  f is a factorization of n Thm*   Thm*  g is a factorization of n Thm*   Thm*  (x:{2..(n+1)}. prime_mset_complete(f)(x) = prime_mset_complete(g)(x)) Thm*   Thm*  f = g	[prime_factorization_limit]
Thm*  f:(Prime), x:. prime(x)  prime_mset_complete(f)(x) = 0	[prime_mset_complete_ismin]
Thm*  f:(Prime), x:Prime. prime_mset_complete(f)(x) = f(x)	[prime_mset_complete_isext]
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]

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