2. b :
3. f : {a..b
}
4. p :
5. is_prime_factorization(a; b; f)
6. prime(p)
7. p |
{a..b}(f)
8. p
{a..b}
9. 0<f(p)
{a..b}(f) = p
{a..b}(reduce_factorization(f; p))
}
{a..b}(f)
{a..b}
{a..b}(f) = p{a..b}(reduce_factorization(f; p))| By: |
Thm*  a,b:, f:({a..b}), z:{a..b}.
Thm* 0<f(z)   {a..b}(f) = z{a..b}(reduce_factorization(f; z))
on [ 0<f(p) ] |
None
About:
 |  |  |  |  |  |  |  |  |  |