Registry · Theorem III.T59 established formalized

III.T59 — Arithmetic Faithfulness

Arith_tr preserves and reflects all arithmetic: addition, multiplication, and GCD. Any τ-theorem about Z/M_k Z translates to valid modular arithmetic in ℤ. Verified at bound 8, depth 3.

Book III Part 9 Ch. 80

Dependency Graph

Depends on (2)

III.D87 III.D88

Depended on by (1)

III.P36

Lean Formalization

Module: TauLib.BookIII.Bridge.TranslationArith

Symbol: arith_faithful_8_3