Registry · Definition I.D12 established formalized

I.D12 — Index Exponentiation

n^m = n * n * ... * n (m times): exponentiation earned by structural recursion on multiplication.

Book I Part 3 Ch. 12

Dependency Graph

Depends on (2)

I.D11 I.D06

Depended on by (3)

I.D13 I.D19c I.P16

Lean Formalization

Module: TauLib.BookI.Denotation.Arithmetic

Symbol: Tau.Denotation.idx_exp