Commit 2025-11-01 10:42 32738718

View on Github →

chore(NumberTheory): add ModEq and Filter version of Dirichlet's theorem (#31139) We add versions of Dirichlet's theorem phrased in terms of naturals and filters, rather than ZMod, for convenience. Since these do not mention ZMod, the usual convention is to avoid use of NeZero and instead use an explicit hypothesis.

Estimated changes