n:
, f,g:(Prime
).
Thm* f is a factorization of n
g is a factorization of n f = gn:, f,g:(Prime).
Thm* f is a factorization of n
Thm*
Thm* g is a factorization of n
Thm*
Thm* (
x:{2..(n+1)
}. prime_mset_complete(f)(x) = prime_mset_complete(g)(x))
Thm*
Thm* f = g
f:(Prime), b:. is_prime_factorization(2; b; prime_mset_complete(f))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 = h