Registry · Definition II.D28 established formalized

II.D28 — Geometric Pi

The circumference-to-diameter ratio of the earned circle S^1, defined as the common limit of inscribed and circumscribed Archimedes polygon perimeters normalized to unit diameter.

Book II Part 5 Ch. 25

Dependency Graph

Depends on (2)

Depended on by (1)

Lean Formalization

Module: TauLib.BookII.Transcendentals.PiEarned

Symbol: pi_circumference