Mathlib Map

Theorems · Definition · number theory

Nat.primesBelow

ℕ → Finset ℕ

primesBelow n is the set of primes less than n as a Finset.

Defined in
Mathlib.NumberTheory.PrimeCounting
Cited by
43 results in Mathlib
Foundations
Depth 54 from the axioms · uses propext, Classical.choice, Quot.sound
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Nat.primesLE · cited by 30Nat.primesLENat.prime_of_mem_primesBelow · cited by 5Nat.prime_of_mem_primesBe…EulerProduct.eulerProduct_hasProd · cited by 4EulerProduct.eulerProduct…Nat.lt_of_mem_primesBelow · cited by 3Nat.lt_of_mem_primesBelowNat.mem_primesBelow · cited by 3Nat.mem_primesBelownot_summable_one_div_on_primes · cited by 2not_summable_one_div_on_p…EulerProduct.eulerProduct_completely_multiplicative · cited by 2EulerProduct.eulerProduct…EulerProduct.norm_tsum_factoredNumbers_sub_tsum_lt · cited by 2EulerProduct.norm_tsum_fa…Nat.primesBelow_one · cited by 2Nat.primesBelow_oneNat.factoredNumbers_compl · cited by 2Nat.factoredNumbers_complNat.smoothNumbersUpTo_card_le · cited by 1Nat.smoothNumbersUpTo_car…Nat.smoothNumbersUpTo_subset_image · cited by 1Nat.smoothNumbersUpTo_sub…Nat.smoothNumbers_eq_factoredNumbers_primesBelow · cited by 1Nat.smoothNumbers_eq_fact…Nat.notMem_primesBelow · cited by 1Nat.notMem_primesBelowNat.roughNumbersUpTo_card_le · cited by 1Nat.roughNumbersUpTo_card…Finset · cited by 13712FinsetNat.Prime · cited by 2059Nat.PrimeFinset.range · cited by 1341Finset.rangeFinset.filter · cited by 949Finset.filterNat.primesBelowCITED BYCITES

Cites4

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Cited by44

Results whose statement or proof uses this declaration.