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 Nat.primesBelow tsum ESeminormedAddCommMonoid.toAddCommMonoid SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing Monoid.toNatPow Nat.instMonoid 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 SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing tsum ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing Monoid.toNatPow Nat.instMonoid Nat.Prime	—	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 SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing tsum ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing Monoid.toNatPow Nat.instMonoid Nat.Prime	—	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 SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing Monoid.toNatPow Nat.instMonoid 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 Nat.primesBelow InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid DivisionCommMonoid.toDivisionMonoid CommGroupWithZero.toDivisionCommMonoid Semifield.toCommGroupWithZero 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 Filter.atTop Nat.instPreorder nhds SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing tsum ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid	—	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 SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid DivisionCommMonoid.toDivisionMonoid CommGroupWithZero.toDivisionCommMonoid Semifield.toCommGroupWithZero SubNegMonoid.toSub AddGroup.toSubNegMonoid NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne NormedRing.toRing NormedCommRing.toNormedRing Nat.Prime tsum ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid	—	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 SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid DivisionCommMonoid.toDivisionMonoid CommGroupWithZero.toDivisionCommMonoid Semifield.toCommGroupWithZero SubNegMonoid.toSub AddGroup.toSubNegMonoid NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne NormedRing.toRing NormedCommRing.toNormedRing Nat.Prime 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 SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing tsum ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing Monoid.toNatPow Nat.instMonoid Nat.Prime	—	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 SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing Set.mulIndicator setOf Nat.Prime tsum ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing Monoid.toNatPow Nat.instMonoid	—	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 SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing tsum ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing Monoid.toNatPow Nat.instMonoid Nat.Prime	—	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	Norm.norm NormedRing.toNorm NormedCommRing.toNormedRing SubNegMonoid.toSub AddGroup.toSubNegMonoid NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup tsum 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	Norm.norm NormedRing.toNorm NormedCommRing.toNormedRing SubNegMonoid.toSub AddGroup.toSubNegMonoid NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup tsum 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 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 tsum ESeminormedAddCommMonoid.toAddCommMonoid SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Monoid.toNatPow Nat.instMonoid	—	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 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 tsum 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_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 SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing Monoid.toNatPow Nat.instMonoid 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 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 tsum Set.Elem Nat.smoothNumbers Set Set.instMembership	—	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 SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing Monoid.toNatPow Nat.instMonoid 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 Set.Elem Nat.factoredNumbers Real.instAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace 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.toNatPow Nat.instMonoid SummationFilter.unconditional	Set.Elem Nat.factoredNumbers Set Set.instMembership HasSum ESeminormedAddCommMonoid.toAddCommMonoid SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing Finset.prod CommRing.toCommMonoid NormedCommRing.toCommRing Finset.filter Nat.Prime Nat.decidablePrime tsum	—	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 Set.Elem Nat.smoothNumbers Real.instAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace 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.toNatPow Nat.instMonoid SummationFilter.unconditional	Set.Elem Nat.smoothNumbers Set Set.instMembership HasSum ESeminormedAddCommMonoid.toAddCommMonoid SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing Finset.prod CommRing.toCommMonoid NormedCommRing.toCommRing Nat.primesBelow tsum	—	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 Real.instOne	—	summable_geometric_iff_norm_lt_one MonoidHom.instMonoidHomClass comp_injective SeminormedAddCommGroup.to_isUniformAddGroup Nat.pow_right_injective

---

← Back to Index