Def  Prime == {x:| prime(x) }

is mentioned by

Thm*  n:{1...}. !f:(Prime). f is a factorization of n	[fta_mset]
Thm*  n:, f,g:(Prime). Thm*  f is a factorization of n  g is a factorization of n  f = g	[prime_factorization_mset_unique]
Thm*  n:{1...}. f:(Prime). f is a factorization of n	[prime_factorization_exists2]
Thm*  f:(Prime), b:. is_prime_factorization(2; b; prime_mset_complete(f))	[prime_mset_c_is_prime_f]
Thm*  f:(Prime), n,n':. Thm*  f is a factorization of n  f is a factorization of n'  n = n'	[only_one_factored_by]
Thm*  f:(Prime), n:. f is a factorization of n  0<n	[only_positives_prime_fed]
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), k:. f is a factorization of k  Prop	[prime_factorization_of_wf]
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]
Thm*  f:(Prime). prime_mset_complete(f)	[prime_mset_complete_wf]
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