Documentation Verification Report

Basic

📁 Source: Mathlib/NumberTheory/EulerProduct/Basic.lean

Statistics

Metric	Count
Definitions	0
Theorems `eulerProduct`, `eulerProduct_hasProd`, `eulerProduct_tprod`, `eulerProduct`, `eulerProduct_completely_multiplicative`, `eulerProduct_completely_multiplicative_hasProd`, `eulerProduct_completely_multiplicative_tprod`, `eulerProduct_hasProd`, `eulerProduct_hasProd_mulIndicator`, `eulerProduct_tprod`, `norm_tsum_factoredNumbers_sub_tsum_lt`, `norm_tsum_smoothNumbers_sub_tsum_lt`, `one_sub_inv_eq_geometric_of_summable_norm`, `prod_filter_prime_geometric_eq_tsum_factoredNumbers`, `prod_filter_prime_tsum_eq_tsum_factoredNumbers`, `prod_primesBelow_geometric_eq_tsum_smoothNumbers`, `prod_primesBelow_tsum_eq_tsum_smoothNumbers`, `summable_and_hasSum_factoredNumbers_prod_filter_prime_geometric`, `summable_and_hasSum_factoredNumbers_prod_filter_prime_tsum`, `summable_and_hasSum_smoothNumbers_prod_primesBelow_geometric`, `summable_and_hasSum_smoothNumbers_prod_primesBelow_tsum`, `norm_lt_one`	22
Total	22

ArithmeticFunction.IsMultiplicative

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`eulerProduct` 📖	mathematical	`ArithmeticFunction.IsMultiplicative` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `NormedCommRing.toCommRing` `Summable` `Real` `Real.instAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `Norm.norm` `NormedRing.toNorm` `NormedCommRing.toNormedRing` `DFunLike.coe` `ArithmeticFunction` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing` `ArithmeticFunction.instFunLikeNat` `SummationFilter.unconditional`	`Filter.Tendsto` `Finset.prod` `CommRing.toCommMonoid` `NormedCommRing.toCommRing` `Nat.primesBelow` `tsum` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `DFunLike.coe` `ArithmeticFunction` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `ArithmeticFunction.instFunLikeNat` `Monoid.toPow` `Nat.instMonoid` `SummationFilter.unconditional` `Filter.atTop` `Nat.instPreorder` `nhds`	—	`EulerProduct.eulerProduct` `ArithmeticFunction.map_zero`
`eulerProduct_hasProd` 📖	mathematical	`ArithmeticFunction.IsMultiplicative` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `NormedCommRing.toCommRing` `Summable` `Real` `Real.instAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `Norm.norm` `NormedRing.toNorm` `NormedCommRing.toNormedRing` `DFunLike.coe` `ArithmeticFunction` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing` `ArithmeticFunction.instFunLikeNat` `SummationFilter.unconditional`	`HasProd` `Nat.Primes` `CommRing.toCommMonoid` `NormedCommRing.toCommRing` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `tsum` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `DFunLike.coe` `ArithmeticFunction` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `ArithmeticFunction.instFunLikeNat` `Monoid.toPow` `Nat.instMonoid` `Nat.Prime` `SummationFilter.unconditional`	—	`EulerProduct.eulerProduct_hasProd` `ArithmeticFunction.map_zero`
`eulerProduct_tprod` 📖	mathematical	`ArithmeticFunction.IsMultiplicative` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `NormedCommRing.toCommRing` `Summable` `Real` `Real.instAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `Norm.norm` `NormedRing.toNorm` `NormedCommRing.toNormedRing` `DFunLike.coe` `ArithmeticFunction` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing` `ArithmeticFunction.instFunLikeNat` `SummationFilter.unconditional`	`tprod` `Nat.Primes` `CommRing.toCommMonoid` `NormedCommRing.toCommRing` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `tsum` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `DFunLike.coe` `ArithmeticFunction` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `ArithmeticFunction.instFunLikeNat` `Monoid.toPow` `Nat.instMonoid` `Nat.Prime` `SummationFilter.unconditional`	—	`EulerProduct.eulerProduct_tprod` `ArithmeticFunction.map_zero`

EulerProduct

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`eulerProduct` 📖	mathematical	`AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `NormedRing.toRing` `NormedCommRing.toNormedRing` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing` `Summable` `Real` `Real.instAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `Norm.norm` `NormedRing.toNorm` `SummationFilter.unconditional` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass`	`Filter.Tendsto` `Finset.prod` `CommRing.toCommMonoid` `NormedCommRing.toCommRing` `Nat.primesBelow` `tsum` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `Monoid.toPow` `Nat.instMonoid` `SummationFilter.unconditional` `Filter.atTop` `Nat.instPreorder` `nhds`	—	`HasProd.tendsto_prod_nat` `eulerProduct_hasProd_mulIndicator` `Finset.prod_mulIndicator_eq_prod_filter`
`eulerProduct_completely_multiplicative` 📖	mathematical	`Summable` `Real` `Real.instAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `Norm.norm` `NormedField.toNorm` `DFunLike.coe` `MonoidWithZeroHom` `Nat.instMulZeroOneClass` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `MonoidWithZeroHom.funLike` `SummationFilter.unconditional`	`Filter.Tendsto` `Finset.prod` `CommRing.toCommMonoid` `Field.toCommRing` `NormedField.toField` `Nat.primesBelow` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `DivisionCommMonoid.toDivisionMonoid` `CommGroupWithZero.toDivisionCommMonoid` `Semifield.toCommGroupWithZero` `Field.toSemifield` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedField.toNormedCommRing` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `NormedRing.toRing` `NormedCommRing.toNormedRing` `DFunLike.coe` `MonoidWithZeroHom` `Nat.instMulZeroOneClass` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `MonoidWithZeroHom.funLike` `Filter.atTop` `Nat.instPreorder` `nhds` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `tsum` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `SummationFilter.unconditional`	—	`MonoidWithZeroHom.map_mul` `HasProd.tendsto_prod_nat` `eulerProduct_hasProd_mulIndicator` `MonoidWithZeroHom.map_one` `MonoidWithZeroHom.map_zero` `Finset.prod_mulIndicator_eq_prod_filter` `Set.mulIndicator_congr` `one_sub_inv_eq_geometric_of_summable_norm` `Finset.prod_congr`
`eulerProduct_completely_multiplicative_hasProd` 📖	mathematical	`Summable` `Real` `Real.instAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `Norm.norm` `NormedField.toNorm` `DFunLike.coe` `MonoidWithZeroHom` `Nat.instMulZeroOneClass` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `MonoidWithZeroHom.funLike` `SummationFilter.unconditional`	`HasProd` `Nat.Primes` `CommRing.toCommMonoid` `Field.toCommRing` `NormedField.toField` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `DivisionCommMonoid.toDivisionMonoid` `CommGroupWithZero.toDivisionCommMonoid` `Semifield.toCommGroupWithZero` `Field.toSemifield` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `NormedRing.toRing` `NormedCommRing.toNormedRing` `DFunLike.coe` `MonoidWithZeroHom` `Nat.instMulZeroOneClass` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `MonoidWithZeroHom.funLike` `Nat.Prime` `tsum` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `SummationFilter.unconditional`	—	`one_sub_inv_eq_geometric_of_summable_norm` `Subtype.prop` `map_pow` `MonoidWithZeroHomClass.toMonoidHomClass` `MonoidWithZeroHom.monoidWithZeroHomClass` `eulerProduct_hasProd` `MonoidWithZeroHom.map_one` `MonoidWithZeroHom.map_mul` `MonoidWithZeroHom.map_zero`
`eulerProduct_completely_multiplicative_tprod` 📖	mathematical	`Summable` `Real` `Real.instAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `Norm.norm` `NormedField.toNorm` `DFunLike.coe` `MonoidWithZeroHom` `Nat.instMulZeroOneClass` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `MonoidWithZeroHom.funLike` `SummationFilter.unconditional`	`tprod` `Nat.Primes` `CommRing.toCommMonoid` `Field.toCommRing` `NormedField.toField` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `DivisionCommMonoid.toDivisionMonoid` `CommGroupWithZero.toDivisionCommMonoid` `Semifield.toCommGroupWithZero` `Field.toSemifield` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `NormedRing.toRing` `NormedCommRing.toNormedRing` `DFunLike.coe` `MonoidWithZeroHom` `Nat.instMulZeroOneClass` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `MonoidWithZeroHom.funLike` `Nat.Prime` `SummationFilter.unconditional` `tsum` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid`	—	`HasProd.tprod_eq` `TopologicalSpace.t2Space_of_metrizableSpace` `EMetricSpace.metrizableSpace` `SummationFilter.instNeBotUnconditional` `eulerProduct_completely_multiplicative_hasProd`
`eulerProduct_hasProd` 📖	mathematical	`AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `NormedRing.toRing` `NormedCommRing.toNormedRing` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing` `Summable` `Real` `Real.instAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `Norm.norm` `NormedRing.toNorm` `SummationFilter.unconditional` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass`	`HasProd` `Nat.Primes` `CommRing.toCommMonoid` `NormedCommRing.toCommRing` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `tsum` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `Monoid.toPow` `Nat.instMonoid` `Nat.Prime` `SummationFilter.unconditional`	—	`hasProd_subtype_iff_mulIndicator` `HasProd.eq_1` `SummationFilter.unconditional.eq_1` `Metric.tendsto_atTop` `norm_tsum_factoredNumbers_sub_tsum_lt` `Summable.of_norm` `Finset.prod_mulIndicator_eq_prod_filter` `dist_eq_norm` `prod_filter_prime_tsum_eq_tsum_factoredNumbers` `norm_sub_rev` `Finset.mem_range` `Nat.lt_of_mem_primesBelow`
`eulerProduct_hasProd_mulIndicator` 📖	mathematical	`AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `NormedRing.toRing` `NormedCommRing.toNormedRing` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing` `Summable` `Real` `Real.instAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `Norm.norm` `NormedRing.toNorm` `SummationFilter.unconditional` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass`	`HasProd` `CommRing.toCommMonoid` `NormedCommRing.toCommRing` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `Set.mulIndicator` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `NormedRing.toRing` `NormedCommRing.toNormedRing` `setOf` `Nat.Prime` `tsum` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `Monoid.toPow` `Nat.instMonoid` `SummationFilter.unconditional`	—	`hasProd_subtype_iff_mulIndicator` `eulerProduct_hasProd`
`eulerProduct_tprod` 📖	mathematical	`AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `NormedRing.toRing` `NormedCommRing.toNormedRing` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing` `Summable` `Real` `Real.instAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `Norm.norm` `NormedRing.toNorm` `SummationFilter.unconditional` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass`	`tprod` `Nat.Primes` `CommRing.toCommMonoid` `NormedCommRing.toCommRing` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `tsum` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `Monoid.toPow` `Nat.instMonoid` `Nat.Prime` `SummationFilter.unconditional`	—	`HasProd.tprod_eq` `TopologicalSpace.t2Space_of_metrizableSpace` `EMetricSpace.metrizableSpace` `SummationFilter.instNeBotUnconditional` `eulerProduct_hasProd`
`norm_tsum_factoredNumbers_sub_tsum_lt` 📖	mathematical	`Summable` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `SummationFilter.unconditional` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `Real` `Real.instLT` `Real.instZero`	`Real` `Real.instLT` `Norm.norm` `NormedRing.toNorm` `NormedCommRing.toNormedRing` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `tsum` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `SummationFilter.unconditional` `Set.Elem` `Nat.factoredNumbers` `Set` `Set.instMembership`	—	`summable_iff_nat_tsum_vanishing` `SeminormedAddCommGroup.to_isUniformAddGroup` `Metric.ball_mem_nhds` `Nat.factoredNumbers_compl` `Summable.tsum_subtype_add_tsum_subtype_compl` `TopologicalSpace.t2Space_of_metrizableSpace` `EMetricSpace.metrizableSpace` `add_sub_cancel_left` `tsum_eq_tsum_diff_singleton`
`norm_tsum_smoothNumbers_sub_tsum_lt` 📖	mathematical	`Summable` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `SummationFilter.unconditional` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `Real` `Real.instLT` `Real.instZero`	`Real` `Real.instLT` `Norm.norm` `NormedRing.toNorm` `NormedCommRing.toNormedRing` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `tsum` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `SummationFilter.unconditional` `Set.Elem` `Nat.smoothNumbers` `Set` `Set.instMembership`	—	`Nat.smoothNumbers_eq_factoredNumbers` `norm_tsum_factoredNumbers_sub_tsum_lt` `Finset.mem_range` `LT.lt.trans_le` `Nat.lt_of_mem_primesBelow`
`one_sub_inv_eq_geometric_of_summable_norm` 📖	mathematical	`Nat.Prime` `Summable` `Real` `Real.instAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `Norm.norm` `NormedField.toNorm` `DFunLike.coe` `MonoidWithZeroHom` `Nat.instMulZeroOneClass` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `MonoidWithZeroHom.funLike` `SummationFilter.unconditional`	`InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `DivisionCommMonoid.toDivisionMonoid` `CommGroupWithZero.toDivisionCommMonoid` `Semifield.toCommGroupWithZero` `Field.toSemifield` `NormedField.toField` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedField.toNormedCommRing` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `NormedRing.toRing` `NormedCommRing.toNormedRing` `DFunLike.coe` `MonoidWithZeroHom` `Nat.instMulZeroOneClass` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `MonoidWithZeroHom.funLike` `tsum` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `Monoid.toPow` `Nat.instMonoid` `SummationFilter.unconditional`	—	`map_pow` `MonoidWithZeroHomClass.toMonoidHomClass` `MonoidWithZeroHom.monoidWithZeroHomClass` `tsum_geometric_of_norm_lt_one` `summable_geometric_iff_norm_lt_one` `Summable.of_norm` `Summable.comp_injective` `instIsUniformAddGroupReal` `Real.instCompleteSpace` `Nat.pow_right_injective` `Nat.Prime.one_lt`
`prod_filter_prime_geometric_eq_tsum_factoredNumbers` 📖	mathematical	`Summable` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `DFunLike.coe` `MonoidHom` `MulOneClass.toMulOne` `Nat.instMulOneClass` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `MonoidHom.instFunLike` `SummationFilter.unconditional`	`Finset.prod` `CommRing.toCommMonoid` `Field.toCommRing` `NormedField.toField` `Finset.filter` `Nat.Prime` `Nat.decidablePrime` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `DivisionCommMonoid.toDivisionMonoid` `CommGroupWithZero.toDivisionCommMonoid` `Semifield.toCommGroupWithZero` `Field.toSemifield` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedField.toNormedCommRing` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `NormedRing.toRing` `NormedCommRing.toNormedRing` `DFunLike.coe` `MonoidHom` `MulOneClass.toMulOne` `Nat.instMulOneClass` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `MonoidHom.instFunLike` `tsum` `Set.Elem` `Nat.factoredNumbers` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `Set` `Set.instMembership` `SummationFilter.unconditional`	—	`HasSum.tsum_eq` `TopologicalSpace.t2Space_of_metrizableSpace` `EMetricSpace.metrizableSpace` `SummationFilter.instNeBotUnconditional` `summable_and_hasSum_factoredNumbers_prod_filter_prime_geometric` `Summable.norm_lt_one` `Nat.Prime.one_lt`
`prod_filter_prime_tsum_eq_tsum_factoredNumbers` 📖	mathematical	`AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `NormedRing.toRing` `NormedCommRing.toNormedRing` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing` `Summable` `Real` `Real.instAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `Norm.norm` `NormedRing.toNorm` `SummationFilter.unconditional`	`Finset.prod` `CommRing.toCommMonoid` `NormedCommRing.toCommRing` `Finset.filter` `Nat.Prime` `Nat.decidablePrime` `tsum` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `Monoid.toPow` `Nat.instMonoid` `SummationFilter.unconditional` `Set.Elem` `Nat.factoredNumbers` `Set` `Set.instMembership`	—	`HasSum.tsum_eq` `TopologicalSpace.t2Space_of_metrizableSpace` `EMetricSpace.metrizableSpace` `SummationFilter.instNeBotUnconditional` `summable_and_hasSum_factoredNumbers_prod_filter_prime_tsum` `Summable.comp_injective` `instIsUniformAddGroupReal` `Real.instCompleteSpace` `Nat.pow_right_injective` `Nat.Prime.one_lt`
`prod_primesBelow_geometric_eq_tsum_smoothNumbers` 📖	mathematical	`Summable` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `DFunLike.coe` `MonoidHom` `MulOneClass.toMulOne` `Nat.instMulOneClass` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `MonoidHom.instFunLike` `SummationFilter.unconditional`	`Finset.prod` `CommRing.toCommMonoid` `Field.toCommRing` `NormedField.toField` `Nat.primesBelow` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `DivisionCommMonoid.toDivisionMonoid` `CommGroupWithZero.toDivisionCommMonoid` `Semifield.toCommGroupWithZero` `Field.toSemifield` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedField.toNormedCommRing` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `NormedRing.toRing` `NormedCommRing.toNormedRing` `DFunLike.coe` `MonoidHom` `MulOneClass.toMulOne` `Nat.instMulOneClass` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `MonoidHom.instFunLike` `tsum` `Set.Elem` `Nat.smoothNumbers` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `Set` `Set.instMembership` `SummationFilter.unconditional`	—	`Nat.smoothNumbers_eq_factoredNumbers` `Nat.primesBelow.eq_1` `prod_filter_prime_geometric_eq_tsum_factoredNumbers`
`prod_primesBelow_tsum_eq_tsum_smoothNumbers` 📖	mathematical	`AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `NormedRing.toRing` `NormedCommRing.toNormedRing` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing` `Summable` `Real` `Real.instAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `Norm.norm` `NormedRing.toNorm` `SummationFilter.unconditional`	`Finset.prod` `CommRing.toCommMonoid` `NormedCommRing.toCommRing` `Nat.primesBelow` `tsum` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `Monoid.toPow` `Nat.instMonoid` `SummationFilter.unconditional` `Set.Elem` `Nat.smoothNumbers` `Set` `Set.instMembership`	—	`HasSum.tsum_eq` `TopologicalSpace.t2Space_of_metrizableSpace` `EMetricSpace.metrizableSpace` `SummationFilter.instNeBotUnconditional` `summable_and_hasSum_smoothNumbers_prod_primesBelow_tsum` `Summable.comp_injective` `instIsUniformAddGroupReal` `Real.instCompleteSpace` `Nat.pow_right_injective` `Nat.Prime.one_lt`
`summable_and_hasSum_factoredNumbers_prod_filter_prime_geometric` 📖	mathematical	`Real` `Real.instLT` `Norm.norm` `NormedField.toNorm` `DFunLike.coe` `MonoidHom` `MulOneClass.toMulOne` `Nat.instMulOneClass` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `MonoidHom.instFunLike` `Real.instOne`	`Summable` `Real` `Set.Elem` `Nat.factoredNumbers` `Real.instAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `Norm.norm` `NormedField.toNorm` `DFunLike.coe` `MonoidHom` `MulOneClass.toMulOne` `Nat.instMulOneClass` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `MonoidHom.instFunLike` `Set` `Set.instMembership` `SummationFilter.unconditional` `HasSum` `ESeminormedAddCommMonoid.toAddCommMonoid` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `Finset.prod` `CommRing.toCommMonoid` `Field.toCommRing` `Finset.filter` `Nat.Prime` `Nat.decidablePrime` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `DivisionCommMonoid.toDivisionMonoid` `CommGroupWithZero.toDivisionCommMonoid` `Semifield.toCommGroupWithZero` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `NormedRing.toRing` `NormedCommRing.toNormedRing`	—	`MonoidHom.map_mul` `Finset.prod_congr` `map_pow` `MonoidHom.instMonoidHomClass` `tsum_geometric_of_norm_lt_one` `Finset.mem_filter` `Summable.of_nonneg_of_le` `norm_nonneg` `norm_pow_le` `NormedDivisionRing.to_normOneClass` `summable_geometric_iff_norm_lt_one` `norm_norm` `summable_and_hasSum_factoredNumbers_prod_filter_prime_tsum` `MonoidHom.map_one`
`summable_and_hasSum_factoredNumbers_prod_filter_prime_tsum` 📖	mathematical	`AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `NormedRing.toRing` `NormedCommRing.toNormedRing` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing` `Summable` `Real` `Real.instAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `Norm.norm` `NormedRing.toNorm` `Monoid.toPow` `Nat.instMonoid` `SummationFilter.unconditional`	`Summable` `Real` `Set.Elem` `Nat.factoredNumbers` `Real.instAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `Norm.norm` `NormedRing.toNorm` `NormedCommRing.toNormedRing` `Set` `Set.instMembership` `SummationFilter.unconditional` `HasSum` `ESeminormedAddCommMonoid.toAddCommMonoid` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `Finset.prod` `CommRing.toCommMonoid` `NormedCommRing.toCommRing` `Finset.filter` `Nat.Prime` `Nat.decidablePrime` `tsum` `Monoid.toPow` `Nat.instMonoid`	—	`Finset.induction` `Nat.factoredNumbers_empty` `Finset.prod_congr` `Finset.filter_true_of_mem` `instIsEmptyFalse` `Set.Finite.summable` `Set.finite_singleton` `hasSum_singleton` `Finset.filter_insert` `Equiv.summable_iff` `Nat.factoredNumbers.map_prime_pow_mul` `Summable.of_nonneg_of_le` `norm_nonneg` `norm_mul_le` `Summable.mul_of_nonneg` `Finset.mem_of_mem_filter` `Finset.prod_insert` `Equiv.hasSum_iff` `Nat.equivProdNatFactoredNumbers_apply'` `instT3Space` `TopologicalSpace.PseudoMetrizableSpace.regularSpace` `PseudoEMetricSpace.pseudoMetrizableSpace` `HasSum.mul` `IsTopologicalRing.toIsTopologicalSemiring` `NonUnitalSeminormedRing.toIsTopologicalRing` `Summable.hasSum` `Summable.of_norm` `summable_mul_of_summable_norm` `Nat.factoredNumbers_insert`
`summable_and_hasSum_smoothNumbers_prod_primesBelow_geometric` 📖	mathematical	`Real` `Real.instLT` `Norm.norm` `NormedField.toNorm` `DFunLike.coe` `MonoidHom` `MulOneClass.toMulOne` `Nat.instMulOneClass` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `MonoidHom.instFunLike` `Real.instOne`	`Summable` `Real` `Set.Elem` `Nat.smoothNumbers` `Real.instAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `Norm.norm` `NormedField.toNorm` `DFunLike.coe` `MonoidHom` `MulOneClass.toMulOne` `Nat.instMulOneClass` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `MonoidHom.instFunLike` `Set` `Set.instMembership` `SummationFilter.unconditional` `HasSum` `ESeminormedAddCommMonoid.toAddCommMonoid` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `Finset.prod` `CommRing.toCommMonoid` `Field.toCommRing` `Nat.primesBelow` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `DivisionCommMonoid.toDivisionMonoid` `CommGroupWithZero.toDivisionCommMonoid` `Semifield.toCommGroupWithZero` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `NormedRing.toRing` `NormedCommRing.toNormedRing`	—	`Nat.smoothNumbers_eq_factoredNumbers` `Nat.primesBelow.eq_1` `summable_and_hasSum_factoredNumbers_prod_filter_prime_geometric`
`summable_and_hasSum_smoothNumbers_prod_primesBelow_tsum` 📖	mathematical	`AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `NormedRing.toRing` `NormedCommRing.toNormedRing` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing` `Summable` `Real` `Real.instAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `Norm.norm` `NormedRing.toNorm` `Monoid.toPow` `Nat.instMonoid` `SummationFilter.unconditional`	`Summable` `Real` `Set.Elem` `Nat.smoothNumbers` `Real.instAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `Norm.norm` `NormedRing.toNorm` `NormedCommRing.toNormedRing` `Set` `Set.instMembership` `SummationFilter.unconditional` `HasSum` `ESeminormedAddCommMonoid.toAddCommMonoid` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `Finset.prod` `CommRing.toCommMonoid` `NormedCommRing.toCommRing` `Nat.primesBelow` `tsum` `Monoid.toPow` `Nat.instMonoid`	—	`Nat.smoothNumbers_eq_factoredNumbers` `Nat.primesBelow.eq_1` `summable_and_hasSum_factoredNumbers_prod_filter_prime_tsum`

Summable

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`norm_lt_one` 📖	mathematical	`Summable` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `NormedRing.toSeminormedRing` `NormedDivisionRing.toNormedRing` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NonUnitalNormedRing.toNormedAddCommGroup` `NormedRing.toNonUnitalNormedRing` `DFunLike.coe` `MonoidHom` `MulOneClass.toMulOne` `Nat.instMulOneClass` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `DivisionSemiring.toSemiring` `DivisionRing.toDivisionSemiring` `NormedDivisionRing.toDivisionRing` `MonoidHom.instFunLike` `SummationFilter.unconditional`	`Real` `Real.instLT` `Norm.norm` `NormedDivisionRing.toNorm` `DFunLike.coe` `MonoidHom` `MulOneClass.toMulOne` `Nat.instMulOneClass` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `DivisionSemiring.toSemiring` `DivisionRing.toDivisionSemiring` `NormedDivisionRing.toDivisionRing` `MonoidHom.instFunLike` `Real.instOne`	—	`summable_geometric_iff_norm_lt_one` `MonoidHom.instMonoidHomClass` `comp_injective` `SeminormedAddCommGroup.to_isUniformAddGroup` `Nat.pow_right_injective`

---

← Back to Index