Registry · Theorem III.T78 established formalized

III.T78 — Radical Primorial 5

rad(M_k) = M_k for k=1..5. Primorial tower is entirely squarefree.

Book III Part 10 Ch. 81

Dependency Graph

Depends on (1)

III.D97

Lean Formalization

Module: TauLib.BookIII.Arithmetic.ABCDeep

Symbol: radical_primorial_5