Registry · Proposition I.P15 established formalized

I.P15 — Sum Zero Iff Both Zero

n + m = 0 iff n = 0 and m = 0. Contrapositive: if either summand is positive, the sum is positive.

Book I Part 3 Ch. 11

Dependency Graph

Depends on (1)

I.D10

Depended on by (1)

I.T14

Lean Formalization

Module: TauLib.BookI.Denotation.Structural

Symbol: Tau.Denotation.tauIdx_sum_zero_iff