Registry · Definition I.D19b established formalized

I.D19b — Internal Primes

p is prime iff p >= 2 and only divisors are 1 and p. P_tau is the set of internal primes; infinite (Euclid's argument earned internally).

Book I Part 4 Ch. 16

Dependency Graph

Depends on (1)

I.D19a

Depended on by (5)

I.D19c I.D19f I.P18 I.T09 III.D95

Lean Formalization

Module: TauLib.BookI.Coordinates.Primes

Symbol: Tau.Coordinates.idx_prime