Registry · Theorem I.T09 established formalized

I.T09 — FTA on tau-Idx

Fundamental Theorem of Arithmetic on tau-Idx: every n >= 2 has a unique prime factorization. Proved via strong induction (existence) and Euclid's Lemma (uniqueness).

Book I Part 4 Ch. 16

Dependency Graph

Depends on (2)

I.D19b I.D11

Depended on by (9)

I.D16 I.D19d I.D31 I.D32 I.D33 III.D97 III.D99 V.T44 V.T99

Lean Formalization

Module: TauLib.BookI.Coordinates.Primes

Symbol: Tau.Coordinates.prime_product_exists, Tau.Coordinates.prime_product_unique