Registry · Theorem I.T15 established formalized

I.T15 — No Ring Negation

No function neg: tau-Idx -> tau-Idx satisfies n + neg(n) = 0 for all n. tau-Idx is a commutative semiring but not a ring.

Book I Part 3 Ch. 11

Dependency Graph

Depends on (1)

I.T14

Lean Formalization

Module: TauLib.BookI.Denotation.Structural

Symbol: Tau.Denotation.tauIdx_no_ring_negation