Registry · Definition II.D10 established formalized

II.D10 — Stage-k Cylinder

The set C_k(x) of all points agreeing with x modulo the k-th primorial P_k. Equivalently, the preimage of the stage-k reduction map at x.

Book II Part 2 Ch. 9

Dependency Graph

Depends on (2)

I.T18 II.D02

Depended on by (18)

II.D11 II.D12 II.D15 II.D17 II.D18a II.D46 II.D47 II.D49 II.D63 II.L01 II.L06 II.P04 II.T04 II.T06 II.T07 II.T18 II.T32 II.T34

Lean Formalization

Module: TauLib.BookII.Domains.Cylinders

Symbol: CylinderDomain