SmoothNumbers

📁 Source: Mathlib/NumberTheory/SmoothNumbers.lean

Statistics

Metric	Count
Definitions `equivProdNatFactoredNumbers`, `equivProdNatSmoothNumbers`, `factoredNumbers`, `instDecidablePredMemSetFactoredNumbers`, `instDecidablePredMemSetSmoothNumbers`, `primesBelow`, `roughNumbersUpTo`, `smoothNumbers`, `smoothNumbersUpTo`	9
Theorems `factoredNumbers_coprime`, `smoothNumbers_coprime`, `eq_prod_primes_mul_sq_of_mem_smoothNumbers`, `equivProdNatFactoredNumbers_apply`, `equivProdNatFactoredNumbers_apply'`, `equivProdNatSmoothNumbers_apply`, `equivProdNatSmoothNumbers_apply'`, `map_prime_pow_mul`, `factoredNumbers_compl`, `factoredNumbers_empty`, `factoredNumbers_insert`, `factoredNumbers_mono`, `lt_of_mem_primesBelow`, `map_prime_pow_mul`, `mem_factoredNumbers`, `mem_factoredNumbers'`, `mem_factoredNumbers_iff_forall_le`, `mem_factoredNumbers_iff_primeFactors_subset`, `mem_factoredNumbers_of_dvd`, `mem_factoredNumbers_of_primeFactors_subset`, `mem_primesBelow`, `mem_smoothNumbers`, `mem_smoothNumbers'`, `mem_smoothNumbersUpTo`, `mem_smoothNumbers_iff_forall_le`, `mem_smoothNumbers_iff_primeFactors_subset`, `mem_smoothNumbers_of_dvd`, `mem_smoothNumbers_of_lt`, `mem_smoothNumbers_of_primeFactors_subset`, `mul_mem_factoredNumbers`, `mul_mem_smoothNumbers`, `ne_zero_of_mem_factoredNumbers`, `ne_zero_of_mem_smoothNumbers`, `notMem_primesBelow`, `pow_mul_mem_factoredNumbers`, `pow_mul_mem_smoothNumbers`, `primeFactors_subset_of_mem_factoredNumbers`, `primeFactors_subset_of_mem_smoothNumbers`, `prime_of_mem_primesBelow`, `primesBelow_succ`, `primesBelow_zero`, `prod_mem_factoredNumbers`, `prod_mem_smoothNumbers`, `roughNumbersUpTo_card_le`, `roughNumbersUpTo_eq_biUnion`, `smoothNumbersUpTo_card_add_roughNumbersUpTo_card`, `smoothNumbersUpTo_card_le`, `smoothNumbersUpTo_subset_image`, `smoothNumbers_compl`, `smoothNumbers_eq_factoredNumbers`, `smoothNumbers_eq_factoredNumbers_primesBelow`, `smoothNumbers_mono`, `smoothNumbers_one`, `smoothNumbers_succ`, `smoothNumbers_zero`	55
Total	64

Nat

Definitions

Name	Category	Theorems
`equivProdNatFactoredNumbers` 📖	CompOp	2 math math: `equivProdNatFactoredNumbers_apply`, `equivProdNatFactoredNumbers_apply'`
`equivProdNatSmoothNumbers` 📖	CompOp	2 math math: `equivProdNatSmoothNumbers_apply'`, `equivProdNatSmoothNumbers_apply`
`factoredNumbers` 📖	CompOp	19 math math: `mem_factoredNumbers'`, `prod_mem_factoredNumbers`, `factoredNumbers_insert`, `smoothNumbers_eq_factoredNumbers_primesBelow`, `factoredNumbers.map_prime_pow_mul`, `mem_factoredNumbers_iff_forall_le`, `factoredNumbers_mono`, `mem_factoredNumbers_of_primeFactors_subset`, `EulerProduct.prod_filter_prime_geometric_eq_tsum_factoredNumbers`, `EulerProduct.summable_and_hasSum_factoredNumbers_prod_filter_prime_geometric`, `EulerProduct.prod_filter_prime_tsum_eq_tsum_factoredNumbers`, `smoothNumbers_eq_factoredNumbers`, `mem_factoredNumbers_iff_primeFactors_subset`, `EulerProduct.norm_tsum_factoredNumbers_sub_tsum_lt`, `factoredNumbers_empty`, `equivProdNatFactoredNumbers_apply'`, `mem_factoredNumbers`, `EulerProduct.summable_and_hasSum_factoredNumbers_prod_filter_prime_tsum`, `factoredNumbers_compl`
`instDecidablePredMemSetFactoredNumbers` 📖	CompOp	—
`instDecidablePredMemSetSmoothNumbers` 📖	CompOp	—
`primesBelow` 📖	CompOp	24 math math: `smoothNumbersUpTo_subset_image`, `roughNumbersUpTo_card_le`, `eq_prod_primes_mul_sq_of_mem_smoothNumbers`, `primeFactors_subset_of_mem_smoothNumbers`, `EulerProduct.eulerProduct_completely_multiplicative`, `smoothNumbers_eq_factoredNumbers_primesBelow`, `roughNumbersUpTo_eq_biUnion`, `EulerProduct.eulerProduct`, `EulerProduct.prod_primesBelow_tsum_eq_tsum_smoothNumbers`, `EulerProduct.summable_and_hasSum_smoothNumbers_prod_primesBelow_geometric`, `EulerProduct.prod_primesBelow_geometric_eq_tsum_smoothNumbers`, `ArithmeticFunction.IsMultiplicative.eulerProduct`, `smoothNumbersUpTo_card_le`, `roughNumbersUpTo_card_le'`, `primesBelow_zero`, `primesBelow_succ`, `riemannZeta_eulerProduct`, `primesBelow_card_eq_primeCounting'`, `EulerProduct.summable_and_hasSum_smoothNumbers_prod_primesBelow_tsum`, `mem_smoothNumbers_iff_primeFactors_subset`, `mem_primesBelow`, `DirichletCharacter.LSeries_eulerProduct`, `notMem_primesBelow`, `one_half_le_sum_primes_ge_one_div`
`roughNumbersUpTo` 📖	CompOp	4 math math: `roughNumbersUpTo_card_le`, `smoothNumbersUpTo_card_add_roughNumbersUpTo_card`, `roughNumbersUpTo_eq_biUnion`, `roughNumbersUpTo_card_le'`
`smoothNumbers` 📖	CompOp	22 math math: `prod_mem_smoothNumbers`, `mem_smoothNumbers_of_lt`, `mem_smoothNumbers'`, `smoothNumbers_eq_factoredNumbers_primesBelow`, `mem_smoothNumbers_iff_forall_le`, `smoothNumbers_succ`, `EulerProduct.prod_primesBelow_tsum_eq_tsum_smoothNumbers`, `EulerProduct.summable_and_hasSum_smoothNumbers_prod_primesBelow_geometric`, `EulerProduct.prod_primesBelow_geometric_eq_tsum_smoothNumbers`, `smoothNumbers_compl`, `smoothNumbers_one`, `smoothNumbers_eq_factoredNumbers`, `equivProdNatSmoothNumbers_apply'`, `mem_smoothNumbers_of_primeFactors_subset`, `EulerProduct.summable_and_hasSum_smoothNumbers_prod_primesBelow_tsum`, `mem_smoothNumbers_iff_primeFactors_subset`, `smoothNumbers_zero`, `map_prime_pow_mul`, `mem_smoothNumbersUpTo`, `smoothNumbers_mono`, `mem_smoothNumbers`, `EulerProduct.norm_tsum_smoothNumbers_sub_tsum_lt`
`smoothNumbersUpTo` 📖	CompOp	4 math math: `smoothNumbersUpTo_subset_image`, `smoothNumbersUpTo_card_add_roughNumbersUpTo_card`, `smoothNumbersUpTo_card_le`, `mem_smoothNumbersUpTo`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`eq_prod_primes_mul_sq_of_mem_smoothNumbers` 📖	mathematical	`Set` `Set.instMembership` `smoothNumbers`	`Finset` `Finset.instMembership` `Finset.powerset` `primesBelow` `Monoid.toNatPow` `instMonoid` `Finset.prod` `instCommMonoid`	—	`sq_mul_squarefree` `mem_smoothNumbers_of_dvd` `Dvd.intro_left` `mem_primesBelow` `mem_smoothNumbers'` `mem_primeFactors` `prod_primeFactors_of_squarefree`
`equivProdNatFactoredNumbers_apply` 📖	mathematical	`Prime` `Finset` `Finset.instMembership` `Set` `Set.instMembership` `factoredNumbers`	`Finset.instInsert` `DFunLike.coe` `Equiv` `Set.Elem` `EquivLike.toFunLike` `Equiv.instEquivLike` `equivProdNatFactoredNumbers` `Monoid.toNatPow` `instMonoid`	—	—
`equivProdNatFactoredNumbers_apply'` 📖	mathematical	`Prime` `Finset` `Finset.instMembership`	`Set` `Set.instMembership` `factoredNumbers` `Finset.instInsert` `DFunLike.coe` `Equiv` `Set.Elem` `EquivLike.toFunLike` `Equiv.instEquivLike` `equivProdNatFactoredNumbers` `Monoid.toNatPow` `instMonoid`	—	—
`equivProdNatSmoothNumbers_apply` 📖	mathematical	`Prime` `Set` `Set.instMembership` `smoothNumbers`	`DFunLike.coe` `Equiv` `Set.Elem` `EquivLike.toFunLike` `Equiv.instEquivLike` `equivProdNatSmoothNumbers` `Monoid.toNatPow` `instMonoid`	—	—
`equivProdNatSmoothNumbers_apply'` 📖	mathematical	`Prime`	`Set` `Set.instMembership` `smoothNumbers` `DFunLike.coe` `Equiv` `Set.Elem` `EquivLike.toFunLike` `Equiv.instEquivLike` `equivProdNatSmoothNumbers` `Monoid.toNatPow` `instMonoid`	—	—
`factoredNumbers_compl` 📖	mathematical	`Finset` `Preorder.toLE` `PartialOrder.toPreorder` `Finset.partialOrder` `primesBelow`	`Set` `Set.instHasSubset` `Set.instSDiff` `Compl.compl` `Set.instCompl` `factoredNumbers` `Set.instSingletonSet` `setOf`	—	`Mathlib.Tactic.Contrapose.contrapose₂` `mem_primesBelow` `prime_of_mem_primeFactorsList` `LE.le.trans` `le_of_mem_primeFactorsList`
`factoredNumbers_empty` 📖	mathematical	—	`factoredNumbers` `Finset` `Finset.instEmptyCollection` `Set` `Set.instSingletonSet`	—	`Set.ext` `ne_and_eq_iff_right` `zero_ne_one`
`factoredNumbers_insert` 📖	mathematical	`Prime`	`factoredNumbers` `Finset` `Finset.instInsert`	—	`Set.ext` `Finset.mem_of_mem_insert_of_ne` `prime_of_mem_primeFactorsList` `Finset.mem_insert_of_mem`
`factoredNumbers_mono` 📖	mathematical	`Finset` `Preorder.toLE` `PartialOrder.toPreorder` `Finset.partialOrder`	`Set` `Set.instHasSubset` `factoredNumbers`	—	—
`lt_of_mem_primesBelow` 📖	—	`Finset` `Finset.instMembership` `primesBelow`	—	—	`Finset.mem_range` `Finset.mem_of_mem_filter`
`map_prime_pow_mul` 📖	mathematical	`Prime`	`Monoid.toNatPow` `instMonoid` `Set` `Set.instMembership` `smoothNumbers`	—	`Prime.smoothNumbers_coprime` `Subtype.mem`
`mem_factoredNumbers` 📖	mathematical	—	`Set` `Set.instMembership` `factoredNumbers` `Finset` `Finset.instMembership`	—	—
`mem_factoredNumbers'` 📖	mathematical	—	`Set` `Set.instMembership` `factoredNumbers` `Finset` `Finset.instMembership`	—	`exists_infinite_primes` `mem_factoredNumbers_iff_forall_le` `lt_irrefl` `Finset.le_sup` `dvd_zero` `lt_one_add` `instZeroLEOneClass` `IsRightCancelAdd.addRightStrictMono_of_addRightMono` `AddRightCancelSemigroup.toIsRightCancelAdd` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `instIsOrderedAddMonoid`
`mem_factoredNumbers_iff_forall_le` 📖	mathematical	—	`Set` `Set.instMembership` `factoredNumbers` `Finset` `Finset.instMembership`	—	—
`mem_factoredNumbers_iff_primeFactors_subset` 📖	mathematical	—	`Set` `Set.instMembership` `factoredNumbers` `Finset` `Finset.instHasSubset` `primeFactors`	—	`ne_zero_of_mem_factoredNumbers` `primeFactors_subset_of_mem_factoredNumbers` `mem_factoredNumbers_of_primeFactors_subset`
`mem_factoredNumbers_of_dvd` 📖	—	`Set` `Set.instMembership` `factoredNumbers`	—	—	`ne_zero_of_dvd_ne_zero` `mem_primeFactorsList` `Dvd.dvd.trans`
`mem_factoredNumbers_of_primeFactors_subset` 📖	mathematical	`Finset` `Finset.instHasSubset` `primeFactors`	`Set` `Set.instMembership` `factoredNumbers`	—	`mem_factoredNumbers` `mem_primeFactors_iff_mem_primeFactorsList`
`mem_primesBelow` 📖	mathematical	—	`Finset` `Finset.instMembership` `primesBelow` `Prime`	—	—
`mem_smoothNumbers` 📖	mathematical	—	`Set` `Set.instMembership` `smoothNumbers`	—	—
`mem_smoothNumbers'` 📖	mathematical	—	`Set` `Set.instMembership` `smoothNumbers`	—	`smoothNumbers_eq_factoredNumbers`
`mem_smoothNumbersUpTo` 📖	mathematical	—	`Finset` `Finset.instMembership` `smoothNumbersUpTo` `Set` `Set.instMembership` `smoothNumbers`	—	`instNoMaxOrder`
`mem_smoothNumbers_iff_forall_le` 📖	mathematical	—	`Set` `Set.instMembership` `smoothNumbers`	—	`smoothNumbers_eq_factoredNumbers`
`mem_smoothNumbers_iff_primeFactors_subset` 📖	mathematical	—	`Set` `Set.instMembership` `smoothNumbers` `Finset` `Finset.instHasSubset` `primeFactors` `primesBelow`	—	`primeFactors_subset_of_mem_smoothNumbers` `mem_smoothNumbers_of_primeFactors_subset` `HasSubset.Subset.trans` `Finset.instIsTransSubset` `Finset.filter_subset`
`mem_smoothNumbers_of_dvd` 📖	—	`Set` `Set.instMembership` `smoothNumbers`	—	—	`smoothNumbers_eq_factoredNumbers` `mem_factoredNumbers_of_dvd`
`mem_smoothNumbers_of_lt` 📖	mathematical	—	`Set` `Set.instMembership` `smoothNumbers`	—	`ne_zero_of_lt` `Finset.mem_range` `lt_of_le_of_lt` `le_of_mem_primeFactorsList` `smoothNumbers_eq_factoredNumbers`
`mem_smoothNumbers_of_primeFactors_subset` 📖	mathematical	`Finset` `Finset.instHasSubset` `primeFactors` `Finset.range`	`Set` `Set.instMembership` `smoothNumbers`	—	`mem_factoredNumbers_of_primeFactors_subset` `smoothNumbers_eq_factoredNumbers`
`mul_mem_factoredNumbers` 📖	—	`Set` `Set.instMembership` `factoredNumbers`	—	—	`primeFactors_subset_of_mem_factoredNumbers` `mem_factoredNumbers_of_primeFactors_subset` `mul_ne_zero` `IsStrictOrderedRing.noZeroDivisors` `instIsStrictOrderedRing` `CanonicallyOrderedAdd.toExistsAddOfLE` `instCanonicallyOrderedAdd` `Finset.union_subset` `primeFactors_mul`
`mul_mem_smoothNumbers` 📖	—	`Set` `Set.instMembership` `smoothNumbers`	—	—	`smoothNumbers_eq_factoredNumbers` `mul_mem_factoredNumbers`
`ne_zero_of_mem_factoredNumbers` 📖	—	`Set` `Set.instMembership` `factoredNumbers`	—	—	—
`ne_zero_of_mem_smoothNumbers` 📖	—	`Set` `Set.instMembership` `smoothNumbers`	—	—	—
`notMem_primesBelow` 📖	mathematical	—	`Finset` `Finset.instMembership` `primesBelow`	—	`LT.lt.false` `lt_of_mem_primesBelow`
`pow_mul_mem_factoredNumbers` 📖	mathematical	`Prime` `Set` `Set.instMembership` `factoredNumbers`	`Finset` `Finset.instInsert` `Monoid.toNatPow` `instMonoid`	—	`pow_ne_zero` `isReduced_of_noZeroDivisors` `IsStrictOrderedRing.noZeroDivisors` `instIsStrictOrderedRing` `CanonicallyOrderedAdd.toExistsAddOfLE` `instCanonicallyOrderedAdd` `Prime.ne_zero` `mul_ne_zero` `mem_primeFactorsList_mul` `prime_dvd_prime_iff_eq` `mem_primeFactorsList` `Prime.dvd_of_dvd_pow` `Finset.mem_insert_self` `Finset.mem_insert_of_mem`
`pow_mul_mem_smoothNumbers` 📖	mathematical	`Set` `Set.instMembership` `smoothNumbers`	`Monoid.toNatPow` `instMonoid`	—	`IsStrictOrderedRing.noZeroDivisors` `instIsStrictOrderedRing` `CanonicallyOrderedAdd.toExistsAddOfLE` `instCanonicallyOrderedAdd` `pow_ne_zero` `isReduced_of_noZeroDivisors` `mul_ne_zero` `mem_primeFactorsList_mul` `Ne.bot_lt` `Prime.dvd_of_dvd_pow` `mem_primeFactorsList` `LT.lt.trans`
`primeFactors_subset_of_mem_factoredNumbers` 📖	mathematical	`Set` `Set.instMembership` `factoredNumbers`	`Finset` `Finset.instHasSubset` `primeFactors`	—	`mem_factoredNumbers` `mem_primeFactors_iff_mem_primeFactorsList`
`primeFactors_subset_of_mem_smoothNumbers` 📖	mathematical	`Set` `Set.instMembership` `smoothNumbers`	`Finset` `Finset.instHasSubset` `primeFactors` `primesBelow`	—	`primeFactors_subset_of_mem_factoredNumbers` `smoothNumbers_eq_factoredNumbers_primesBelow`
`prime_of_mem_primesBelow` 📖	mathematical	`Finset` `Finset.instMembership` `primesBelow`	`Prime`	—	`Finset.mem_filter`
`primesBelow_succ` 📖	mathematical	—	`primesBelow` `Finset` `Prime` `decidablePrime` `Finset.instInsert`	—	`primesBelow.eq_1` `Finset.range_add_one` `Finset.filter_insert`
`primesBelow_zero` 📖	mathematical	—	`primesBelow` `Finset` `Finset.instEmptyCollection`	—	`primesBelow.eq_1` `Finset.range_zero` `Finset.filter_empty`
`prod_mem_factoredNumbers` 📖	mathematical	—	`Set` `Set.instMembership` `factoredNumbers` `instOne` `Finset` `Finset.instMembership` `Finset.decidableMem` `primeFactorsList`	—	`List.prod_ne_zero` `instNontrivial` `IsStrictOrderedRing.noZeroDivisors` `instIsStrictOrderedRing` `CanonicallyOrderedAdd.toExistsAddOfLE` `instCanonicallyOrderedAdd` `LT.lt.false` `pos_of_mem_primeFactorsList` `List.mem_of_mem_filter` `mem_primeFactorsList` `List.of_mem_filter` `mem_list_primes_of_dvd_prod` `instIsCancelMulZero` `Unique.instSubsingleton` `Prime.prime` `prime_of_mem_primeFactorsList`
`prod_mem_smoothNumbers` 📖	mathematical	—	`Set` `Set.instMembership` `smoothNumbers` `instOne` `primeFactorsList`	—	`smoothNumbers_eq_factoredNumbers`
`roughNumbersUpTo_card_le` 📖	mathematical	—	`Finset.card` `roughNumbersUpTo` `Finset.sum` `instAddCommMonoid` `Finset` `Finset.instSDiff` `primesBelow`	—	`roughNumbersUpTo_eq_biUnion` `LE.le.trans` `Finset.card_biUnion_le` `Finset.sum_le_sum` `IsOrderedAddMonoid.toAddLeftMono` `instIsOrderedAddMonoid` `Eq.le` `card_multiples'`
`roughNumbersUpTo_eq_biUnion` 📖	mathematical	—	`roughNumbersUpTo` `Finset.biUnion` `Finset` `Finset.instSDiff` `primesBelow` `Finset.filter` `Finset.range`	—	`Finset.ext` `Finset.filter.congr_simp` `not_lt`
`smoothNumbersUpTo_card_add_roughNumbersUpTo_card` 📖	mathematical	—	`Finset.card` `smoothNumbersUpTo` `roughNumbersUpTo`	—	`smoothNumbersUpTo.eq_1` `roughNumbersUpTo.eq_1` `Finset.card_union_of_disjoint` `Finset.disjoint_filter` `Finset.filter_union_right` `Finset.filter_ne'` `Finset.card_erase_of_mem` `Finset.mem_range_succ_iff` `Finset.card_range` `tsub_zero` `instOrderedSub` `ne_zero_of_mem_smoothNumbers` `Finset.filter_congr`
`smoothNumbersUpTo_card_le` 📖	mathematical	—	`Finset.card` `smoothNumbersUpTo` `Monoid.toNatPow` `instMonoid` `primesBelow`	—	`Finset.card_product` `Finset.card_powerset` `Finset.card_erase_of_mem` `Finset.card_range` `tsub_zero` `instOrderedSub` `LE.le.trans` `Finset.card_le_card` `smoothNumbersUpTo_subset_image` `Finset.card_image_le`
`smoothNumbersUpTo_subset_image` 📖	mathematical	—	`Finset` `Finset.instHasSubset` `smoothNumbersUpTo` `Finset.image` `Monoid.toNatPow` `instMonoid` `Finset.prod` `instCommMonoid` `SProd.sprod` `Finset.instSProd` `Finset.powerset` `primesBelow` `Finset.erase` `Finset.range`	—	`mem_smoothNumbersUpTo` `eq_prod_primes_mul_sq_of_mem_smoothNumbers` `Finset.prod_congr` `Finset.mem_powerset` `ne_zero_of_mem_smoothNumbers` `IsStrictOrderedRing.noZeroDivisors` `instIsStrictOrderedRing` `CanonicallyOrderedAdd.toExistsAddOfLE` `instCanonicallyOrderedAdd` `isReduced_of_noZeroDivisors` `le_sqrt'` `LE.le.trans` `mul_one` `mul_le_mul_right` `instMulLeftMono` `Finset.one_le_prod'` `Prime.one_le` `prime_of_mem_primesBelow`
`smoothNumbers_compl` 📖	mathematical	—	`Set` `Set.instHasSubset` `Set.instSDiff` `Compl.compl` `Set.instCompl` `smoothNumbers` `Set.instSingletonSet` `setOf`	—	`smoothNumbers_eq_factoredNumbers` `factoredNumbers_compl` `Finset.filter_subset`
`smoothNumbers_eq_factoredNumbers` 📖	mathematical	—	`smoothNumbers` `factoredNumbers` `Finset.range`	—	—
`smoothNumbers_eq_factoredNumbers_primesBelow` 📖	mathematical	—	`smoothNumbers` `factoredNumbers` `primesBelow`	—	`smoothNumbers_eq_factoredNumbers` `Set.Subset.antisymm` `mem_primesBelow` `Finset.mem_range` `factoredNumbers_mono` `Finset.mem_of_mem_filter`
`smoothNumbers_mono` 📖	mathematical	—	`Set` `Set.instHasSubset` `smoothNumbers`	—	`LT.lt.trans_le`
`smoothNumbers_one` 📖	mathematical	—	`smoothNumbers` `Set` `Set.instSingletonSet`	—	`smoothNumbers_succ` `smoothNumbers_zero`
`smoothNumbers_succ` 📖	mathematical	`Prime`	`smoothNumbers`	—	`smoothNumbers_eq_factoredNumbers` `Finset.range_add_one` `factoredNumbers_insert`
`smoothNumbers_zero` 📖	mathematical	—	`smoothNumbers` `Set` `Set.instSingletonSet`	—	`smoothNumbers_eq_factoredNumbers` `factoredNumbers_empty`

Nat.Prime

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`factoredNumbers_coprime` 📖	—	`Nat.Prime` `Finset` `Finset.instMembership` `Set` `Set.instMembership` `Nat.factoredNumbers`	—	—	`coprime_iff_not_dvd` `Nat.mem_primeFactorsList_iff_dvd`
`smoothNumbers_coprime` 📖	—	`Nat.Prime` `Set` `Set.instMembership` `Nat.smoothNumbers`	—	—	`factoredNumbers_coprime` `Finset.notMem_range_self` `Nat.smoothNumbers_eq_factoredNumbers`

Nat.factoredNumbers

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`map_prime_pow_mul` 📖	mathematical	`Nat.Prime` `Finset` `Finset.instMembership`	`Monoid.toNatPow` `Nat.instMonoid` `Set` `Set.instMembership` `Nat.factoredNumbers`	—	`Nat.Prime.factoredNumbers_coprime` `Subtype.mem`

---

← Back to Index