FTA Sections DiscrMathExt Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
RankTheoremName
20Thm*  a:b:f:({a..b}), p:.
Thm*  is_prime_factorization(abf)
Thm*  
Thm*  prime(p)
Thm*  
Thm*  p | {a..b}(f {a..b}(f) = p{a..b}(reduce_factorization(fp))
[remove_prime_factor]
cites the following:
19Thm*  a:b:f:({a..b}), p:.
Thm*  is_prime_factorization(abf)
Thm*  
Thm*  prime(p p | {a..b}(f p  {a..b} & 0<f(p)
[prime_factorization_includes_prime_divisors]
6Thm*  a,b:f:({a..b}), z:{a..b}.
Thm*  0<f(z {a..b}(f) = z{a..b}(reduce_factorization(fz))
[eval_factorization_pluck]
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
FTA Sections DiscrMathExt Doc