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))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)a,b:, f:({a..b}), z:{a..b}.
Thm* 0<f(z)
{a..b}(f) = z{a..b}(reduce_factorization(f; z))