Registry · Proposition I.P06 established formalized

I.P06 — Arithmetic Laws

tau-Idx with index addition and multiplication forms a commutative semiring: commutativity, associativity, distributivity, identity elements.

Book I Part 3 Ch. 11

Dependency Graph

Depends on (2)

I.D10 I.D11

Lean Formalization

Module: TauLib.BookI.Denotation.Arithmetic

Symbol: Tau.Denotation.arithmetic_laws