Registry · Proposition III.P42 established formalized

III.P42 — Sieve-CRT Compatibility

Sieve-CRT compatibility: n divisible by p_i iff i-th CRT residue is 0. Multiplicative sieve = product of local sieves.

Book III Part 10 Ch. 81

Dependency Graph

Depends on (2)

III.D99 III.T10

Lean Formalization

Module: TauLib.BookIII.Spectral.SieveInfrastructure

Symbol: sieve_crt_compat_3