Registry · Definition I.D10 established formalized

I.D10 — Index Addition

n + m = rho^m(n): addition on tau-Idx earned by iterating rho m times starting from n. No Peano axioms imported.

Book I Part 3 Ch. 11

Dependency Graph

Depends on (3)

I.D07 I.D06 I.D02

Depended on by (9)

I.D11 I.D19a I.D35 I.P06 I.P15 I.P16 I.P17 I.P18 I.T14

Lean Formalization

Module: TauLib.BookI.Denotation.Arithmetic

Symbol: Tau.Denotation.idx_add