Registry · Theorem III.T10 tau-effective formalized

III.T10 — CRT Decomposition Theorem

τ-native Chinese Remainder Theorem: ℤ/Prim(k)ℤ ≅ ∏ᵢ₌₁ᵏ ℤ/pᵢℤ proved constructively without signed arithmetic. Uses modular Bézout via K3 divisibility. CRT = algebraic Euler product: End(F) ≅ ∏ End(ℤ/pᵢℤ).

Book III Part 3 Ch. 15

Dependency Graph

Depends on (2)

III.D19 III.T09

Depended on by (20)

III.D107 III.D20 III.D22 III.D23 III.D26 III.D33 III.D34 III.D55 III.D59 III.P05 III.P07 III.P12 III.P22 III.P42 III.P43 III.R09 III.T11 III.T14 III.T16 III.T21

Lean Formalization

Module: TauLib.BookIII.Spectral.CRT

Symbol: crt_spectral_check