Source indexedtheorem · leanprover/lean4:v4.32.0

dirichlet_thm

PrimeNumberTheoremAnd.Consequences · PrimeNumberTheoremAnd/Consequences.lean:2514 to 2534

Mathematical statement

Exact Lean statement

@[blueprint
  (title := "Dirichlet's theorem")
  (statement := /-- Any primitive residue class contains an infinite number of primes. -/)
  (proof := /--
  If this were not the case, then the sum $\sum_{p \leq x: p = a\ (q)} \log p$
  would be bounded in $x$, contradicting Theorem \ref{chebyshev-asymptotic-pnt}.
  -/)
  (proofUses := ["chebyshev-asymptotic-pnt"])
  (latexEnv := "corollary")]
theorem dirichlet_thm {q : ℕ} {a : ℕ} (hq : q ≥ 1) (ha : Nat.Coprime a q) (ha' : a < q) :
    Infinite { p // p.Prime ∧ p % q = a }

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

@[blueprint  (title := "Dirichlet's theorem")  (statement := /-- Any primitive residue class contains an infinite number of primes. -/)  (proof := /--  If this were not the case, then the sum $\sum_{p \leq x: p = a\ (q)} \log p$  would be bounded in $x$, contradicting Theorem \ref{chebyshev-asymptotic-pnt}.  -/)  (proofUses := ["chebyshev-asymptotic-pnt"])  (latexEnv := "corollary")]theorem dirichlet_thm {q : ℕ} {a : ℕ} (hq : q ≥ 1) (ha : Nat.Coprime a q) (ha' : a < q) :    Infinite { p // p.Prime ∧ p % q = a } := by  have : {p | p.Prime ∧ p % q = a}.Infinite := by    have : {p | p.Prime ∧ p ≡ a [MOD q]}.Infinite := by      have := @infinite_setOf_prime_and_eq_mod      specialize @this q <| NeZero.of_pos hq      simp_all only [isUnit_iff_exists_inv, forall_exists_index, ← ZMod.natCast_eq_natCast_iff]      exact this (IsUnit.exists_right_inv (show IsUnit (a : ZMod q) from by        rwa [ZMod.isUnit_iff_coprime])).choose (IsUnit.exists_right_inv (show IsUnit (a : ZMod q)          from by rwa [ZMod.isUnit_iff_coprime])).choose_spec    exact this.mono fun p hp ↦ ⟨hp.1, by simpa [ModEq, mod_eq_of_lt ha'] using hp.2⟩  exact Set.infinite_coe_iff.mpr this