Registry · Definition I.D98 tau-effective formalized

I.D98 — Galois Group of Primorial Stage

The Galois group at stage k is (Z/M_k Z)×, the group of units. Its order is φ(M_k) = ∏(p_i - 1) for primes p_i ≤ p_k. Verified: φ(2)=1, φ(6)=2, φ(30)=8.

Book I Part 18 Ch. 85

Dependency Graph

Depends on (2)

Depended on by (2)

Lean Formalization

Module: TauLib.BookI.Boundary.Galois

Symbol: galois_group_order