Commit 2024-11-25 17:36 dee58f26

View on Github →

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

Estimated changes

Modified Mathlib/NumberTheory/LSeries/PrimesInAP.lean

added theorem ArithmeticFunction.vonMangoldt.LSeries_residueClass_lower_bound

added theorem ArithmeticFunction.vonMangoldt.LfunctionResidueClassAux_real

added theorem ArithmeticFunction.vonMangoldt.continuousOn_LfunctionResidueClassAux'

added theorem ArithmeticFunction.vonMangoldt.continuousOn_LfunctionResidueClassAux

added theorem ArithmeticFunction.vonMangoldt.eqOn_LfunctionResidueClassAux

added theorem ArithmeticFunction.vonMangoldt.not_summable_residueClass_prime_div

added theorem Nat.forall_exists_prime_gt_and_eq_mod

added theorem Nat.setOf_prime_and_eq_mod_infinite

Modified docs/100.yaml