Registry · Proposition I.P18 established formalized

I.P18 — Zero Vacuous

Zero is vacuous: (1) not prime, (2) not a successor, (3) divisible by everything, (4) unique multiplicative absorber. A non-participant rather than a destructive element.

Book I Part 4 Ch. 16

Dependency Graph

Depends on (4)

Depended on by (1)

Lean Formalization

Module: TauLib.BookI.Denotation.Structural

Symbol: Tau.Denotation.tauIdx_zero_not_prime