Commit 2025-11-01 16:26 09125ff9

View on Github →

chore: fix names of Dirichlet's theorems (#31146)

Estimated changes

Modified Mathlib/NumberTheory/LSeries/PrimesInAP.lean

added theorem Nat.frequently_atTop_prime_and_modEq

deleted theorem Nat.frequently_atTop_prime_and_modEq_one

added theorem Nat.infinite_setOf_prime_and_eq_mod

added theorem Nat.infinite_setOf_prime_and_modEq

deleted theorem Nat.infinite_setOf_prime_and_modEq_one

deleted theorem Nat.setOf_prime_and_eq_mod_infinite

Modified docs/100.yaml

Modified docs/1000.yaml