Theorems · Theorem · number theory
Nat.frequently_atTop_modEq_one
∀ {k : ℕ}, k ≠ 0 → ∃ᶠ (p : ℕ) in Filter.atTop, Nat.Prime p ∧ p ≡ 1 [MOD k]- Defined in
- Mathlib.NumberTheory.PrimesCongruentOne
- Cited by
- 1 results in Mathlib
- Foundations
- Depth 217 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites7
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Filter.atTopstatement · cited by 2,405
- LT.lt.leproof · cited by 2,189
- Nat.Primestatement and proof · cited by 2,059
- Filter.Frequentlystatement · cited by 414
- Nat.ModEqstatement and proof · cited by 225
- Filter.frequently_atTopproof · cited by 14
- Nat.exists_prime_gt_modEq_oneproof · cited by 1
Cited by1
Results whose statement or proof uses this declaration.
- Nat.infinite_setOfPred_prime_modEq_oneproof · cited by 1