Registry · Definition I.D11 established formalized

I.D11 — Index Multiplication

n * m = n + n + ... + n (m times): multiplication earned by structural recursion on addition.

Book I Part 3 Ch. 11

Dependency Graph

Depends on (2)

I.D10 I.D06

Depended on by (9)

I.D12 I.D19a I.D35 I.P06 I.P16 I.P18 I.P19 I.T09 I.T16

Lean Formalization

Module: TauLib.BookI.Denotation.Arithmetic

Symbol: Tau.Denotation.idx_mul