Theorem Nat.forall_exists_prime_gt_and_eq_mod

Modification history

2024-11-25 17:36

Mathlib/NumberTheory/LSeries/PrimesInAP.lean

feat(NumberTheory/LSeries/PrimesInAP): proof of Dirichlet's Theorem (#19421)

Added Nat.forall_exists_prime_gt_and_eq_mod View on Github →