Registry · Definition III.D88 established formalized

III.D88 — CRT-Integer Correspondence

CRT decomposition x ↦ (x mod p_1, ..., x mod p_k) and reconstruction. Roundtrip verified: decompose then reconstruct = identity. This is the classical CRT on the primorial tower.

Book III Part 9 Ch. 80

Dependency Graph

Depends on (1)

Depended on by (1)

Lean Formalization

Module: TauLib.BookIII.Bridge.TranslationArith

Symbol: crt_reconstruct