Registry · Definition III.D101 established formalized

III.D101 — Brun Sieve Count

Brun sieve: count integers in [1..n] coprime to first d primes. Inclusion-exclusion at depth d. B(30,3)=8=φ(30).

Book III Part 10 Ch. 81

Dependency Graph

Depends on (1)

III.D99

Depended on by (1)

III.T67

Lean Formalization

Module: TauLib.BookIII.Spectral.SieveInfrastructure

Symbol: brun_sieve_count