Theorems · Definition · number theory
Nat.factoredNumbers
Finset ℕ → Set ℕ
factoredNumbers s, for a finite set s of natural numbers, is the set of positive natural
numbers all of whose prime factors are in s.
- Defined in
- Mathlib.NumberTheory.SmoothNumbers
- Cited by
- 33 results in Mathlib
- Foundations
- Depth 74 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites4
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Setstatement · cited by 53,352
- Finsetstatement and proof · cited by 13,712
- Set.ofPredproof · cited by 6,101
- Nat.primeFactorsListproof · cited by 105
Cited by34
Results whose statement or proof uses this declaration.
- Nat.smoothNumbers_eq_factoredNumbersstatement · cited by 16
- Nat.equivProdNatFactoredNumbersstatement and proof · cited by 4
- EulerProduct.eulerProduct_hasProdproof · cited by 4
- Nat.primeFactors_subset_of_mem_factoredNumbersstatement and proof · cited by 3
- EulerProduct.summable_and_hasSum_factoredNumbers_prod_filter_prime_tsumstatement and proof · cited by 3
- Nat.mem_factoredNumbers_of_primeFactors_subsetstatement · cited by 3
- EulerProduct.norm_tsum_factoredNumbers_sub_tsum_ltstatement and proof · cited by 2
- EulerProduct.summable_and_hasSum_factoredNumbers_prod_filter_prime_geometricstatement · cited by 2
- Nat.mem_factoredNumbersstatement · cited by 2
- Nat.Prime.factoredNumbers_coprimestatement and proof · cited by 2
- Nat.factoredNumbers_complstatement and proof · cited by 2
- Nat.factoredNumbers_emptystatement · cited by 2