a:{2...}, b:
, g,h:({a..b
}
).
Thm* is_prime_factorization(a; b; g)
Thm*
Thm* is_prime_factorization(a; b; h)
{a..b}(g) = {a..b}(h) g = ha:, 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}), j:{a..b}. 0<f(j) j | {a..b}(f)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,g:({a..b}), j:{a..b}.
Thm* 0<f(j)
Thm*
Thm* 0<g(j)
reduce_factorization(f; j) = reduce_factorization(g; j) f = ga:
, b:, f:({a..b}). {a..b}(f) a:, b:, f:({a..b}), j:{a..b}.
Thm* 2
j 0<f(j) {a..b}(reduce_factorization(f; j))<{a..b}(f)a,b:, f:({a..b}), j:{a..b}.
Thm* 0<f(j)
Thm*
Thm* is_prime_factorization(a; b; f)
Thm*
Thm* is_prime_factorization(a; b; reduce_factorization(f; j))
a:{2...}, b:, f:({a..b}). {a..b}(f) = 1 
f = (
x.0)a:{2...}, b:, f:({a..b}). {a..b}(f) = 1 
(
i:{a..b}. 0<f(i))