Registry · Definition I.D19a established formalized

I.D19a — Internal Divisibility

a | b iff exists k in tau-Idx such that b = a * k. Decidable, reflexive, transitive. First relational concept earned from Part III arithmetic.

Book I Part 4 Ch. 16

Dependency Graph

Depends on (2)

I.D10 I.D11

Depended on by (5)

I.D19b I.D31 I.D32 I.P10 I.P18

Lean Formalization

Module: TauLib.BookI.Coordinates.Primes

Symbol: Tau.Coordinates.idx_divides