Registry · Proposition I.P44 tau-effective formalized

I.P44 — CRT-Galois Decomposition

The Galois group decomposes via CRT: Gal_k ≅ ∏(Z/p_i Z)× for i=1..k. Order equality φ(M_k) = ∏(p_i-1) verified computationally at stages 1-3.

Book I Part 18 Ch. 85

Dependency Graph

Depends on (2)

I.D98 I.T45

Lean Formalization

Module: TauLib.BookI.Boundary.Galois

Symbol: galois_crt_3