Registry · Definition III.D110 tau-effective formalized

III.D110 — Squarefree ABC Check

For squarefree coprime pairs: c ≤ rad(abc). Trivially true since rad(n)=n for squarefree n.

Book III Part 10 Ch. 81

Dependency Graph

Depends on (1)

III.D97

Depended on by (2)

III.P47 III.T77

Lean Formalization

Module: TauLib.BookIII.Arithmetic.ABCDeep

Symbol: squarefree_abc_check