Registry · Proposition III.P47 established formalized

III.P47 — Squarefree Dominance Theorem

ABC trivially true for squarefree coprime triples: rad(abc)=abc≥c. Quality q<1 always. Zero high-quality among squarefree coprimes.

Book III Part 10 Ch. 81

Dependency Graph

Depends on (2)

III.D110 III.T77

Depended on by (1)

III.P48

Lean Formalization

Module: TauLib.BookIII.Arithmetic.ABCDeep

Symbol: squarefree_dominance_thm