Def  b | a == c:. a = bc

is mentioned by

Thm*  a:, b:, f:({a..b}), p:. Thm*  is_prime_factorization(a; b; f) Thm*   Thm*  prime(p) Thm*   Thm*  p | {a..b}(f)  {a..b}(f) = p{a..b}(reduce_factorization(f; p))	[remove_prime_factor]
Thm*  a:, b:, f:({a..b}), p:. Thm*  is_prime_factorization(a; b; f) Thm*   Thm*  prime(p)  p | {a..b}(f)  p  {a..b} & 0<f(p)	[prime_factorization_includes_prime_divisors]
Thm*  p:. prime(p)  (b,z:. p | zb  b  0 & p | z)	[prime_divs_exp]
Thm*  p:.  Thm*  prime(p) Thm*   Thm*  (a,b:, e:({a..b}). Thm*  (a<b  p | ( i:{a..b}. e(i))  (i:{a..b}. p | e(i)))	[prime_divs_mul_via_intseg]
Thm*  X:. prime(X)  (a,b:. X | ab  X | a  X | b)	[nat_prime_div_each_factor]
Thm*  X:.  Thm*  prime(X) Thm*   Thm*  (X1:. X1<X  prime(X1)  (a,b:. X1 | ab  X1 | a  X1 | b)) Thm*   Thm*  (W:. 0<W  W<X  (t:. X | tW  X | t))	[nat_prime_div_each_factorLEMMA]
Thm*  a,b:, f:({a..b}), j:{a..b}. 0<f(j)  j | {a..b}(f)	[factor_divides_evalfactorization]

In prior sections: num thy 1 SimpleMulFacts IteratedBinops

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