FactorizationStarter

The fundamental theorem of arithmetic in use

Open in Workbench View on GitHub

1-- The fundamental theorem of arithmetic in use2-- Part of Cumulus, the Grace17 mathematics library.3-- Copyright (c) 2026 Grant Passmore.4-- Released under the Apache License 2.0. See LICENSE in the repository root.5-- Authors: Grant Passmore67module FactorizationStarter8import Grace.Cumulus.NumberTheory910-- A factorization is a list of primes; its product is computed by recursion.11theorem twelve12  shows ∏ [2, 2, 3] = 1213proof14  compute1516-- Multiplicities say how many times a prime is used.17theorem twelve.twos18  shows multiplicity(2, [2, 2, 3]) = 219proof20  compute2122-- Every positive natural number has a prime factorization.23theorem factorization_exists (n : Nat)24  requires positive : n ≠ 025  shows ∃ xs, List(ℕ, xs) ∧ PrimeList(xs) ∧ ∏ xs = n26proof27  exact primeFactorization.exists at n with *2829-- Two prime factorizations of the same number use every prime equally often.30theorem factorization_unique (xs ys : List(ℕ)) (q : Nat)31  requires primesXs : PrimeList(xs)32  requires primesYs : PrimeList(ys)33  requires equal : ∏ xs = ∏ ys34  shows multiplicity(q, xs) = multiplicity(q, ys)35proof36  have unique := primeFactorization.unique at xs with *37  exact unique with ys, assumption, primesXs, primesYs, equal, q, assumption3839-- Euclid's lemma, the step that makes uniqueness work.40theorem euclid (p a b : Nat)41  requires prime : Prime(p)42  requires divides : p ∣ a * b43  shows p ∣ a ∨ p ∣ b44proof45  exact Prime.divides_mul at p, a, b with *46