Registry · Proposition III.P05 tau-effective formalized

III.P05 — Independence of Prime-Level Actions

Prime-level actions T^(i) on ℤ/pᵢℤ are independent. CRT guarantees unique reassembly into global action on ℤ/Prim(k)ℤ. The τ-incarnation of the local-global principle.

Book III Part 3 Ch. 15

Dependency Graph

Depends on (1)

III.T10

Depended on by (3)

III.D33 III.P12 III.T21

Lean Formalization

Module: TauLib.BookIII.Spectral.CRT

Symbol: prime_independence_check