Nuprl - FTA LEMMAs for only_one_factored

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html

Rank	Theorem	Name
6	Thm* f:(Prime), n,n':. Thm* f is a factorization of n f is a factorization of n' n = n'	[only_one_factored_by]
cites the following:
5	Thm* f:(Prime), n:. f is a factorization of n 0<n	[only_positives_prime_fed]
4	Thm* a,c,b:, f:({a..b}). Thm* ac cb {a..b}(f) = {a..c}(f){c..b}(f)	[eval_factorization_split_mid]
5	Thm* a:{2...}, b:, f:({a..b}). {a..b}(f) = 1 (i:{a..b}. f(i) = 0)	[eval_factorization_one]
0	Thm* f:(Prime), x:Prime. prime_mset_complete(f)(x) = f(x)	[prime_mset_complete_isext]
0	Thm* f:(Prime), x:. prime(x) prime_mset_complete(f)(x) = 0	[prime_mset_complete_ismin]

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html