NatInt

📁 Source: Mathlib/Topology/Algebra/InfiniteSum/NatInt.lean

Statistics

Metric	Count
Definitions	0
Theorems even_mul_odd, int_rec, nat_mul_neg, nat_mul_neg_add_one, of_add_one_of_neg_add_one, of_nat_of_neg, of_nat_of_neg_add_one, prod_range_mul, tendsto_prod_nat, zero_mul, even_add_odd, int_rec, nat_add_neg, nat_add_neg_add_one, of_add_one_of_neg_add_one, of_nat_of_neg, of_nat_of_neg_add_one, sum_range_add, tendsto_sum_nat, zero_add, comp_nat_add, even_mul_odd, hasProd_iff_tendsto_nat, int_rec, nat_mul_neg, nat_mul_neg_add_one, nat_tprod_vanishing, of_add_one_of_neg_add_one, of_nat_of_neg, of_nat_of_neg_add_one, prod_mul_tprod_nat_add, prod_mul_tprod_nat_mul', tendsto_atTop_one, tendsto_prod_tprod_nat, tprod_eq_zero_mul, tprod_of_nat_of_neg, alternating, comp_nat_add, even_add_odd, hasSum_iff_tendsto_nat, int_rec, nat_add_neg, nat_add_neg_add_one, nat_tsum_vanishing, of_add_one_of_neg_add_one, of_nat_of_neg, of_nat_of_neg_add_one, sum_add_tsum_nat_add, sum_add_tsum_nat_add', tendsto_atTop_zero, tendsto_sum_tsum_nat, tsum_eq_zero_add, tsum_of_nat_of_neg, cauchySeq_finset_iff_nat_tprod_vanishing, cauchySeq_finset_iff_nat_tsum_vanishing, hasProd_nat_add_iff, hasProd_nat_add_iff', hasSum_nat_add_iff, hasSum_nat_add_iff', multipliable_iff_nat_tprod_vanishing, multipliable_int_iff_multipliable_nat_and_neg, multipliable_int_iff_multipliable_nat_and_neg_add_one, multipliable_nat_add_iff, multipliable_pnat_iff_multipliable_nat, multipliable_pnat_iff_multipliable_succ, pnat_multipliable_iff_multipliable_succ, rel_iSup_prod, rel_iSup_sum, rel_iSup_tprod, rel_iSup_tsum, rel_sup_add, rel_sup_mul, summable_iff_nat_tsum_vanishing, summable_int_iff_summable_nat_and_neg, summable_int_iff_summable_nat_and_neg_add_zero, summable_nat_add_iff, summable_pnat_iff_summable_nat, summable_pnat_iff_summable_succ, tendsto_prod_nat_add, tendsto_sum_nat_add, tprod_eq_zero_mul', tprod_even_mul_odd, tprod_iSup_decode₂, tprod_iUnion_decode₂, tprod_int_eq_zero_mul_tprod_pnat, tprod_int_eq_zero_mul_tprod_pnat_sq, tprod_int_rec, tprod_nat_mul_neg, tprod_nat_mul_neg_add_one, tprod_of_add_one_of_neg_add_one, tprod_of_nat_of_neg_add_one, tprod_pnat_eq_tprod_succ, tprod_zero_pnat_eq_tprod_nat, tsum_eq_zero_add', tsum_even_add_odd, tsum_iSup_decode₂, tsum_iUnion_decode₂, tsum_int_eq_zero_add_tsum_pnat, tsum_int_eq_zero_add_two_mul_tsum_pnat, tsum_int_rec, tsum_nat_add_neg, tsum_nat_add_neg_add_one, tsum_of_add_one_of_neg_add_one, tsum_of_nat_of_neg_add_one, tsum_pnat_eq_tsum_succ, tsum_zero_pnat_eq_tsum_nat	106
Total	106

HasProd

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
even_mul_odd 📖	mathematical	HasProd SummationFilter.unconditional	MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass CommMonoid.toMonoid	—	mul_right_injective₀ IsCancelMulZero.toIsLeftCancelMulZero Nat.instIsCancelMulZero two_ne_zero' Function.Injective.hasProd_range_iff add_left_injective AddRightCancelSemigroup.toIsRightCancelAdd mul_isCompl range_two_mul range_two_mul_add_one Nat.isCompl_even_odd
int_rec 📖	mathematical	HasProd SummationFilter.unconditional	MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass CommMonoid.toMonoid	—	of_nat_of_neg_add_one
nat_mul_neg 📖	mathematical	HasProd SummationFilter.unconditional	MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass CommMonoid.toMonoid	—	hasProd_of_prod_eq le_total Finset.mem_image Int.natCast_natAbs Int.instIsOrderedAddMonoid abs_of_nonpos Int.instAddLeftMono neg_neg Finset.prod_mul_distrib Finset.prod_subset_one_on_sdiff Finset.inter_subset_union Finset.prod_union_inter Finset.prod_image Int.instCharZero mul hasProd_ite_eq SummationFilter.instLeAtTopUnconditional
nat_mul_neg_add_one 📖	mathematical	HasProd SummationFilter.unconditional	MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass CommMonoid.toMonoid	—	hasProd_of_prod_eq Function.Injective.injOn Nat.cast_injective Int.instCharZero Finset.prod_union Finset.prod_image Finset.prod_mul_distrib
of_add_one_of_neg_add_one 📖	mathematical	HasProd SummationFilter.unconditional	MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass CommMonoid.toMonoid	—	of_nat_of_neg_add_one zero_mul mul_comm
of_nat_of_neg 📖	mathematical	HasProd CommGroup.toCommMonoid SummationFilter.unconditional	DivInvMonoid.toDiv Group.toDivInvMonoid CommGroup.toGroup MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid	—	of_nat_of_neg_add_one IsTopologicalGroup.toContinuousMul neg_zero Nat.cast_zero Finset.prod_range_one hasProd_nat_add_iff' mul_div_assoc'
of_nat_of_neg_add_one 📖	mathematical	HasProd SummationFilter.unconditional	MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass CommMonoid.toMonoid	—	disjoint_iff_inf_le codisjoint_iff_le_sup Int.instCharZero mul_isCompl Function.Injective.hasProd_range_iff Nat.cast_injective
prod_range_mul 📖	mathematical	HasProd SummationFilter.unconditional	MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass CommMonoid.toMonoid Finset.prod Finset.range	—	mul_compl Finset.hasProd SummationFilter.instLeAtTopUnconditional Equiv.hasProd_iff
tendsto_prod_nat 📖	mathematical	HasProd SummationFilter.unconditional	Filter.Tendsto Finset.prod Finset.range Filter.atTop Nat.instPreorder nhds	—	Filter.Tendsto.comp Filter.tendsto_finset_range
zero_mul 📖	mathematical	HasProd SummationFilter.unconditional	MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass CommMonoid.toMonoid	—	Finset.prod_range_one prod_range_mul

HasSum

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
even_add_odd 📖	mathematical	HasSum SummationFilter.unconditional	AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid	—	mul_right_injective₀ IsCancelMulZero.toIsLeftCancelMulZero Nat.instIsCancelMulZero two_ne_zero' Function.Injective.hasSum_range_iff add_left_injective AddRightCancelSemigroup.toIsRightCancelAdd add_isCompl range_two_mul range_two_mul_add_one Nat.isCompl_even_odd
int_rec 📖	mathematical	HasSum SummationFilter.unconditional	AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid	—	of_nat_of_neg_add_one
nat_add_neg 📖	mathematical	HasSum SummationFilter.unconditional	AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid	—	hasSum_of_sum_eq Finset.mem_union Finset.mem_image le_total Int.natCast_natAbs abs_eq_self Int.instIsOrderedAddMonoid abs_of_nonpos Int.instAddLeftMono neg_neg Finset.sum_add_distrib Finset.sum_subset_zero_on_sdiff Finset.inter_subset_union Finset.mem_sdiff neg_eq_zero Finset.mem_inter Finset.sum_union_inter Finset.sum_image Set.injOn_of_eq_iff_eq Int.instCharZero add hasSum_ite_eq SummationFilter.instLeAtTopUnconditional
nat_add_neg_add_one 📖	mathematical	HasSum SummationFilter.unconditional	AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid	—	hasSum_of_sum_eq Function.Injective.injOn Nat.cast_injective Int.instCharZero Finset.mem_union Finset.mem_image Finset.mem_preimage Finset.sum_union Finset.disjoint_iff_ne Finset.sum_image Finset.sum_add_distrib
of_add_one_of_neg_add_one 📖	mathematical	HasSum SummationFilter.unconditional	AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid	—	of_nat_of_neg_add_one zero_add add_comm
of_nat_of_neg 📖	mathematical	HasSum AddCommGroup.toAddCommMonoid SummationFilter.unconditional	SubNegMonoid.toSub AddGroup.toSubNegMonoid AddCommGroup.toAddGroup AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid	—	of_nat_of_neg_add_one IsTopologicalAddGroup.toContinuousAdd neg_zero Nat.cast_zero Finset.sum_range_one hasSum_nat_add_iff' add_sub_assoc'
of_nat_of_neg_add_one 📖	mathematical	HasSum SummationFilter.unconditional	AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid	—	disjoint_iff_inf_le codisjoint_iff_le_sup Set.mem_univ Set.mem_union Set.mem_range Int.instCharZero add_isCompl Function.Injective.hasSum_range_iff Nat.cast_injective
sum_range_add 📖	mathematical	HasSum SummationFilter.unconditional	AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid Finset.sum Finset.range	—	add_compl Finset.hasSum SummationFilter.instLeAtTopUnconditional Equiv.hasSum_iff
tendsto_sum_nat 📖	mathematical	HasSum SummationFilter.unconditional	Filter.Tendsto Finset.sum Finset.range Filter.atTop Nat.instPreorder nhds	—	Filter.Tendsto.comp Filter.tendsto_finset_range
zero_add 📖	mathematical	HasSum SummationFilter.unconditional	AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid	—	Finset.sum_range_one sum_range_add

Multipliable

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
comp_nat_add 📖	—	Multipliable SummationFilter.unconditional	—	—	HasProd.multipliable HasProd.prod_range_mul hasProd
even_mul_odd 📖	—	Multipliable SummationFilter.unconditional	—	—	HasProd.multipliable HasProd.even_mul_odd hasProd
hasProd_iff_tendsto_nat 📖	mathematical	Multipliable SummationFilter.unconditional	HasProd Filter.Tendsto Finset.prod Finset.range Filter.atTop Nat.instPreorder nhds	—	HasProd.tendsto_prod_nat tendsto_nhds_unique Filter.atTop_neBot instIsDirectedOrder IsStrictOrderedRing.toIsOrderedRing Nat.instIsStrictOrderedRing instArchimedeanNat hasProd
int_rec 📖	—	Multipliable SummationFilter.unconditional	—	—	of_nat_of_neg_add_one
nat_mul_neg 📖	mathematical	Multipliable SummationFilter.unconditional	MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass CommMonoid.toMonoid	—	HasProd.multipliable HasProd.nat_mul_neg hasProd
nat_mul_neg_add_one 📖	mathematical	Multipliable SummationFilter.unconditional	MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass CommMonoid.toMonoid	—	HasProd.multipliable HasProd.nat_mul_neg_add_one hasProd
nat_tprod_vanishing 📖	mathematical	Multipliable CommGroup.toCommMonoid SummationFilter.unconditional Set Filter Filter.instMembership nhds InvOneClass.toOne DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid DivisionCommMonoid.toDivisionMonoid CommGroup.toDivisionCommMonoid	Set.instMembership tprod Set.Elem	—	isUniformGroup_of_commGroup cauchySeq_finset_iff_nat_tprod_vanishing Filter.Tendsto.cauchySeq hasProd
of_add_one_of_neg_add_one 📖	—	Multipliable SummationFilter.unconditional	—	—	HasProd.multipliable HasProd.of_add_one_of_neg_add_one hasProd
of_nat_of_neg 📖	—	Multipliable CommGroup.toCommMonoid SummationFilter.unconditional	—	—	HasProd.multipliable HasProd.of_nat_of_neg hasProd
of_nat_of_neg_add_one 📖	—	Multipliable SummationFilter.unconditional	—	—	HasProd.multipliable HasProd.of_nat_of_neg_add_one hasProd
prod_mul_tprod_nat_add 📖	mathematical	Multipliable CommGroup.toCommMonoid SummationFilter.unconditional	MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid CommGroup.toGroup Finset.prod Finset.range tprod	—	prod_mul_tprod_nat_mul' IsTopologicalGroup.toContinuousMul multipliable_nat_add_iff
prod_mul_tprod_nat_mul' 📖	mathematical	Multipliable SummationFilter.unconditional	MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass CommMonoid.toMonoid Finset.prod Finset.range tprod	—	HasProd.tprod_eq SummationFilter.instNeBotUnconditional HasProd.prod_range_mul hasProd
tendsto_atTop_one 📖	mathematical	Multipliable CommGroup.toCommMonoid SummationFilter.unconditional	Filter.Tendsto Filter.atTop Nat.instPreorder nhds InvOneClass.toOne DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid DivisionCommMonoid.toDivisionMonoid CommGroup.toDivisionCommMonoid	—	Nat.cofinite_eq_atTop tendsto_cofinite_one
tendsto_prod_tprod_nat 📖	mathematical	Multipliable SummationFilter.unconditional	Filter.Tendsto Finset.prod Finset.range Filter.atTop Nat.instPreorder nhds tprod	—	HasProd.tendsto_prod_nat hasProd
tprod_eq_zero_mul 📖	mathematical	Multipliable CommGroup.toCommMonoid SummationFilter.unconditional	tprod MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid CommGroup.toGroup	—	tprod_eq_zero_mul' IsTopologicalGroup.toContinuousMul multipliable_nat_add_iff
tprod_of_nat_of_neg 📖	mathematical	Multipliable CommGroup.toCommMonoid SummationFilter.unconditional	tprod DivInvMonoid.toDiv Group.toDivInvMonoid CommGroup.toGroup MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid	—	HasProd.tprod_eq SummationFilter.instNeBotUnconditional HasProd.of_nat_of_neg hasProd

Summable

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
alternating 📖	mathematical	Summable NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing UniformSpace.toTopologicalSpace SummationFilter.unconditional	Distrib.toMul NonUnitalNonAssocSemiring.toDistrib Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Ring.toAddCommGroup AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne	—	even_add_odd IsTopologicalAddGroup.toContinuousAdd IsUniformAddGroup.to_topologicalAddGroup Even.neg_pow Distrib.rightDistribClass Nat.instAtLeastTwoHAddOfNat one_pow one_mul comp_injective mul_right_injective₀ IsCancelMulZero.toIsLeftCancelMulZero Nat.instIsCancelMulZero two_ne_zero' pow_add pow_one mul_neg mul_one neg_mul neg add_left_injective AddRightCancelSemigroup.toIsRightCancelAdd
comp_nat_add 📖	—	Summable SummationFilter.unconditional	—	—	HasSum.summable HasSum.sum_range_add hasSum
even_add_odd 📖	—	Summable SummationFilter.unconditional	—	—	HasSum.summable HasSum.even_add_odd hasSum
hasSum_iff_tendsto_nat 📖	mathematical	Summable SummationFilter.unconditional	HasSum Filter.Tendsto Finset.sum Finset.range Filter.atTop Nat.instPreorder nhds	—	HasSum.tendsto_sum_nat tendsto_nhds_unique Filter.atTop_neBot instIsDirectedOrder IsStrictOrderedRing.toIsOrderedRing Nat.instIsStrictOrderedRing instArchimedeanNat hasSum
int_rec 📖	—	Summable SummationFilter.unconditional	—	—	of_nat_of_neg_add_one
nat_add_neg 📖	mathematical	Summable SummationFilter.unconditional	AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid	—	HasSum.summable HasSum.nat_add_neg hasSum
nat_add_neg_add_one 📖	mathematical	Summable SummationFilter.unconditional	AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid	—	HasSum.summable HasSum.nat_add_neg_add_one hasSum
nat_tsum_vanishing 📖	mathematical	Summable AddCommGroup.toAddCommMonoid SummationFilter.unconditional Set Filter Filter.instMembership nhds NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	Set.instMembership tsum Set.Elem	—	isUniformAddGroup_of_addCommGroup cauchySeq_finset_iff_nat_tsum_vanishing Filter.Tendsto.cauchySeq hasSum
of_add_one_of_neg_add_one 📖	—	Summable SummationFilter.unconditional	—	—	HasSum.summable HasSum.of_add_one_of_neg_add_one hasSum
of_nat_of_neg 📖	—	Summable AddCommGroup.toAddCommMonoid SummationFilter.unconditional	—	—	HasSum.summable HasSum.of_nat_of_neg hasSum
of_nat_of_neg_add_one 📖	—	Summable SummationFilter.unconditional	—	—	HasSum.summable HasSum.of_nat_of_neg_add_one hasSum
sum_add_tsum_nat_add 📖	mathematical	Summable AddCommGroup.toAddCommMonoid SummationFilter.unconditional	AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup Finset.sum Finset.range tsum	—	sum_add_tsum_nat_add' IsTopologicalAddGroup.toContinuousAdd summable_nat_add_iff
sum_add_tsum_nat_add' 📖	mathematical	Summable SummationFilter.unconditional	AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid Finset.sum Finset.range tsum	—	HasSum.tsum_eq SummationFilter.instNeBotUnconditional HasSum.sum_range_add hasSum
tendsto_atTop_zero 📖	mathematical	Summable AddCommGroup.toAddCommMonoid SummationFilter.unconditional	Filter.Tendsto Filter.atTop Nat.instPreorder nhds NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	—	Nat.cofinite_eq_atTop tendsto_cofinite_zero
tendsto_sum_tsum_nat 📖	mathematical	Summable SummationFilter.unconditional	Filter.Tendsto Finset.sum Finset.range Filter.atTop Nat.instPreorder nhds tsum	—	HasSum.tendsto_sum_nat hasSum
tsum_eq_zero_add 📖	mathematical	Summable AddCommGroup.toAddCommMonoid SummationFilter.unconditional	tsum AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup	—	tsum_eq_zero_add' IsTopologicalAddGroup.toContinuousAdd summable_nat_add_iff
tsum_of_nat_of_neg 📖	mathematical	Summable AddCommGroup.toAddCommMonoid SummationFilter.unconditional	tsum SubNegMonoid.toSub AddGroup.toSubNegMonoid AddCommGroup.toAddGroup AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid	—	HasSum.tsum_eq SummationFilter.instNeBotUnconditional HasSum.of_nat_of_neg hasSum

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
cauchySeq_finset_iff_nat_tprod_vanishing 📖	mathematical	—	CauchySeq Finset PartialOrder.toPreorder Finset.partialOrder Finset.prod CommGroup.toCommMonoid Set Set.instMembership tprod Set.Elem UniformSpace.toTopologicalSpace SummationFilter.unconditional	—	cauchySeq_finset_iff_tprod_vanishing Set.disjoint_left LE.le.not_gt Finset.le_max' le_of_not_gt Finset.mem_range
cauchySeq_finset_iff_nat_tsum_vanishing 📖	mathematical	—	CauchySeq Finset PartialOrder.toPreorder Finset.partialOrder Finset.sum AddCommGroup.toAddCommMonoid Set Set.instMembership tsum Set.Elem UniformSpace.toTopologicalSpace SummationFilter.unconditional	—	cauchySeq_finset_iff_tsum_vanishing Set.disjoint_left LE.le.not_gt Finset.le_max' le_of_not_gt Finset.mem_range
hasProd_nat_add_iff 📖	mathematical	—	HasProd CommGroup.toCommMonoid SummationFilter.unconditional MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid CommGroup.toGroup Finset.prod Finset.range	—	Equiv.hasProd_iff coe_notMemRangeEquiv_symm Finset.hasProd_compl_iff
hasProd_nat_add_iff' 📖	mathematical	—	HasProd CommGroup.toCommMonoid DivInvMonoid.toDiv Group.toDivInvMonoid CommGroup.toGroup Finset.prod Finset.range SummationFilter.unconditional	—	div_mul_cancel
hasSum_nat_add_iff 📖	mathematical	—	HasSum AddCommGroup.toAddCommMonoid SummationFilter.unconditional AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup Finset.sum Finset.range	—	Equiv.hasSum_iff coe_notMemRangeEquiv_symm Finset.hasSum_compl_iff
hasSum_nat_add_iff' 📖	mathematical	—	HasSum AddCommGroup.toAddCommMonoid SubNegMonoid.toSub AddGroup.toSubNegMonoid AddCommGroup.toAddGroup Finset.sum Finset.range SummationFilter.unconditional	—	hasSum_nat_add_iff sub_add_cancel
multipliable_iff_nat_tprod_vanishing 📖	mathematical	—	Multipliable CommGroup.toCommMonoid UniformSpace.toTopologicalSpace SummationFilter.unconditional Set Set.instMembership tprod Set.Elem	—	multipliable_iff_cauchySeq_finset cauchySeq_finset_iff_nat_tprod_vanishing
multipliable_int_iff_multipliable_nat_and_neg 📖	mathematical	—	Multipliable CommGroup.toCommMonoid UniformSpace.toTopologicalSpace SummationFilter.unconditional	—	Multipliable.comp_injective Nat.cast_injective Int.instCharZero neg_injective Multipliable.of_nat_of_neg IsUniformGroup.to_topologicalGroup
multipliable_int_iff_multipliable_nat_and_neg_add_one 📖	mathematical	—	Multipliable CommGroup.toCommMonoid UniformSpace.toTopologicalSpace SummationFilter.unconditional	—	Multipliable.comp_injective Nat.cast_injective Int.instCharZero Multipliable.of_nat_of_neg_add_one IsTopologicalGroup.toContinuousMul IsUniformGroup.to_topologicalGroup
multipliable_nat_add_iff 📖	mathematical	—	Multipliable CommGroup.toCommMonoid SummationFilter.unconditional	—	Function.Surjective.multipliable_iff_of_hasProd_iff Equiv.surjective hasProd_nat_add_iff
multipliable_pnat_iff_multipliable_nat 📖	mathematical	—	Multipliable PNat CommGroup.toCommMonoid PNat.val SummationFilter.unconditional	—	multipliable_pnat_iff_multipliable_succ multipliable_nat_add_iff
multipliable_pnat_iff_multipliable_succ 📖	mathematical	—	Multipliable PNat PNat.val SummationFilter.unconditional	—	Equiv.multipliable_iff
pnat_multipliable_iff_multipliable_succ 📖	mathematical	—	Multipliable PNat PNat.val SummationFilter.unconditional	—	multipliable_pnat_iff_multipliable_succ
rel_iSup_prod 📖	mathematical	Bot.bot OrderBot.toBot Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice BoundedOrder.toOrderBot CompleteLattice.toBoundedOrder MulOne.toOne MulOneClass.toMulOne Monoid.toMulOneClass CommMonoid.toMonoid iSup ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice tprod SummationFilter.unconditional	Finset Finset.instMembership Finset.prod	—	iSup_subtype' Finset.tprod_subtype rel_iSup_tprod Finite.to_countable Finite.of_fintype
rel_iSup_sum 📖	mathematical	Bot.bot OrderBot.toBot Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice BoundedOrder.toOrderBot CompleteLattice.toBoundedOrder AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid iSup ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice tsum SummationFilter.unconditional	Finset Finset.instMembership Finset.sum	—	iSup_subtype' Finset.tsum_subtype rel_iSup_tsum Finite.to_countable Finite.of_fintype
rel_iSup_tprod 📖	—	Bot.bot OrderBot.toBot Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice BoundedOrder.toOrderBot CompleteLattice.toBoundedOrder MulOne.toOne MulOneClass.toMulOne Monoid.toMulOneClass CommMonoid.toMonoid iSup ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice tprod SummationFilter.unconditional	—	—	nonempty_encodable Encodable.iSup_decode₂ tprod_iSup_decode₂
rel_iSup_tsum 📖	—	Bot.bot OrderBot.toBot Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice BoundedOrder.toOrderBot CompleteLattice.toBoundedOrder AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid iSup ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice tsum SummationFilter.unconditional	—	—	nonempty_encodable Encodable.iSup_decode₂ tsum_iSup_decode₂
rel_sup_add 📖	mathematical	Bot.bot OrderBot.toBot Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice BoundedOrder.toOrderBot CompleteLattice.toBoundedOrder AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid iSup ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice tsum SummationFilter.unconditional	SemilatticeSup.toMax ConditionallyCompleteLattice.toLattice AddZero.toAdd	—	iSup_bool_eq tsum_fintype SummationFilter.instLeAtTopUnconditional Fintype.sum_bool rel_iSup_tsum Bool.countable
rel_sup_mul 📖	mathematical	Bot.bot OrderBot.toBot Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice BoundedOrder.toOrderBot CompleteLattice.toBoundedOrder MulOne.toOne MulOneClass.toMulOne Monoid.toMulOneClass CommMonoid.toMonoid iSup ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice tprod SummationFilter.unconditional	SemilatticeSup.toMax ConditionallyCompleteLattice.toLattice MulOne.toMul	—	iSup_bool_eq tprod_fintype SummationFilter.instLeAtTopUnconditional Fintype.prod_bool rel_iSup_tprod Bool.countable
summable_iff_nat_tsum_vanishing 📖	mathematical	—	Summable AddCommGroup.toAddCommMonoid UniformSpace.toTopologicalSpace SummationFilter.unconditional Set Set.instMembership tsum Set.Elem	—	summable_iff_cauchySeq_finset cauchySeq_finset_iff_nat_tsum_vanishing
summable_int_iff_summable_nat_and_neg 📖	mathematical	—	Summable AddCommGroup.toAddCommMonoid UniformSpace.toTopologicalSpace SummationFilter.unconditional	—	Summable.comp_injective Nat.cast_injective Int.instCharZero neg_injective Summable.of_nat_of_neg IsUniformAddGroup.to_topologicalAddGroup
summable_int_iff_summable_nat_and_neg_add_zero 📖	mathematical	—	Summable AddCommGroup.toAddCommMonoid UniformSpace.toTopologicalSpace SummationFilter.unconditional	—	Summable.comp_injective Nat.cast_injective Int.instCharZero Summable.of_nat_of_neg_add_one IsTopologicalAddGroup.toContinuousAdd IsUniformAddGroup.to_topologicalAddGroup
summable_nat_add_iff 📖	mathematical	—	Summable AddCommGroup.toAddCommMonoid SummationFilter.unconditional	—	Function.Surjective.summable_iff_of_hasSum_iff Equiv.surjective hasSum_nat_add_iff
summable_pnat_iff_summable_nat 📖	mathematical	—	Summable PNat AddCommGroup.toAddCommMonoid PNat.val SummationFilter.unconditional	—	summable_pnat_iff_summable_succ summable_nat_add_iff
summable_pnat_iff_summable_succ 📖	mathematical	—	Summable PNat PNat.val SummationFilter.unconditional	—	Equiv.summable_iff
tendsto_prod_nat_add 📖	mathematical	—	Filter.Tendsto tprod CommGroup.toCommMonoid SummationFilter.unconditional Filter.atTop Nat.instPreorder nhds InvOneClass.toOne DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid DivisionCommMonoid.toDivisionMonoid CommGroup.toDivisionCommMonoid	—	div_eq_iff_eq_mul mul_comm Multipliable.prod_mul_tprod_nat_add tendsto_const_nhds div_self' Filter.Tendsto.div' IsTopologicalGroup.to_continuousDiv HasProd.tendsto_prod_nat Multipliable.hasProd Filter.Tendsto.congr tprod_eq_one_of_not_multipliable multipliable_nat_add_iff
tendsto_sum_nat_add 📖	mathematical	—	Filter.Tendsto tsum AddCommGroup.toAddCommMonoid SummationFilter.unconditional Filter.atTop Nat.instPreorder nhds NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	—	sub_eq_iff_eq_add add_comm Summable.sum_add_tsum_nat_add tendsto_const_nhds sub_self Filter.Tendsto.sub IsTopologicalAddGroup.to_continuousSub HasSum.tendsto_sum_nat Summable.hasSum Filter.Tendsto.congr tsum_eq_zero_of_not_summable summable_nat_add_iff
tprod_eq_zero_mul' 📖	mathematical	Multipliable SummationFilter.unconditional	tprod MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass CommMonoid.toMonoid	—	Finset.prod_range_one Multipliable.prod_mul_tprod_nat_mul'
tprod_even_mul_odd 📖	mathematical	Multipliable SummationFilter.unconditional	MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass CommMonoid.toMonoid tprod	—	HasProd.tprod_eq SummationFilter.instNeBotUnconditional HasProd.even_mul_odd Multipliable.hasProd
tprod_iSup_decode₂ 📖	mathematical	Bot.bot OrderBot.toBot Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice BoundedOrder.toOrderBot CompleteLattice.toBoundedOrder MulOne.toOne MulOneClass.toMulOne Monoid.toMulOneClass CommMonoid.toMonoid	tprod iSup ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice Encodable.decode₂ SummationFilter.unconditional	—	tprod_extend_one Encodable.encode_injective tprod_congr em iSup_congr_Prop Encodable.decode₂_encode iSup_iSup_eq_right Function.Injective.extend_apply Function.extend_apply' Encodable.decode₂_ne_none_iff iSup_neg iSup_bot
tprod_iUnion_decode₂ 📖	mathematical	Set Set.instEmptyCollection MulOne.toOne MulOneClass.toMulOne Monoid.toMulOneClass CommMonoid.toMonoid	tprod Set.iUnion Encodable.decode₂ SummationFilter.unconditional	—	tprod_iSup_decode₂
tprod_int_eq_zero_mul_tprod_pnat 📖	mathematical	Multipliable CommGroup.toCommMonoid UniformSpace.toTopologicalSpace SummationFilter.unconditional	tprod MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid CommGroup.toGroup PNat PNat.val	—	multipliable_int_iff_multipliable_nat_and_neg multipliable_pnat_iff_multipliable_succ multipliable_nat_add_iff IsUniformGroup.to_topologicalGroup tprod_nat_mul_neg IsTopologicalGroup.toContinuousMul tprod_zero_pnat_eq_tprod_nat Multipliable.mul Nat.cast_zero neg_zero mul_comm mul_assoc LeftCancelSemigroup.toIsLeftCancelMul Multipliable.tprod_mul SummationFilter.instNeBotUnconditional
tprod_int_eq_zero_mul_tprod_pnat_sq 📖	mathematical	Function.Even Multipliable CommGroup.toCommMonoid UniformSpace.toTopologicalSpace SummationFilter.unconditional	tprod MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid CommGroup.toGroup Monoid.toNatPow PNat PNat.val	—	sq tprod_int_eq_zero_mul_tprod_pnat
tprod_int_rec 📖	mathematical	Multipliable SummationFilter.unconditional	tprod MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass CommMonoid.toMonoid	—	HasProd.tprod_eq SummationFilter.instNeBotUnconditional Multipliable.hasProd
tprod_nat_mul_neg 📖	mathematical	Multipliable SummationFilter.unconditional	tprod MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass CommMonoid.toMonoid	—	HasProd.tprod_eq SummationFilter.instNeBotUnconditional HasProd.nat_mul_neg Multipliable.hasProd
tprod_nat_mul_neg_add_one 📖	mathematical	Multipliable SummationFilter.unconditional	tprod MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass CommMonoid.toMonoid	—	HasProd.tprod_eq SummationFilter.instNeBotUnconditional HasProd.nat_mul_neg_add_one Multipliable.hasProd
tprod_of_add_one_of_neg_add_one 📖	mathematical	Multipliable SummationFilter.unconditional	tprod MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass CommMonoid.toMonoid	—	HasProd.tprod_eq SummationFilter.instNeBotUnconditional HasProd.of_add_one_of_neg_add_one Multipliable.hasProd
tprod_of_nat_of_neg_add_one 📖	mathematical	Multipliable SummationFilter.unconditional	tprod MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass CommMonoid.toMonoid	—	HasProd.tprod_eq SummationFilter.instNeBotUnconditional HasProd.of_nat_of_neg_add_one Multipliable.hasProd
tprod_pnat_eq_tprod_succ 📖	mathematical	—	tprod PNat PNat.val SummationFilter.unconditional	—	Equiv.tprod_eq
tprod_zero_pnat_eq_tprod_nat 📖	mathematical	Multipliable CommGroup.toCommMonoid SummationFilter.unconditional	MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid CommGroup.toGroup tprod PNat PNat.val	—	Multipliable.tprod_eq_zero_mul LeftCancelSemigroup.toIsLeftCancelMul tprod_pnat_eq_tprod_succ
tsum_eq_zero_add' 📖	mathematical	Summable SummationFilter.unconditional	tsum AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid	—	Finset.sum_range_one Summable.sum_add_tsum_nat_add'
tsum_even_add_odd 📖	mathematical	Summable SummationFilter.unconditional	AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid tsum	—	HasSum.tsum_eq SummationFilter.instNeBotUnconditional HasSum.even_add_odd Summable.hasSum
tsum_iSup_decode₂ 📖	mathematical	Bot.bot OrderBot.toBot Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice BoundedOrder.toOrderBot CompleteLattice.toBoundedOrder AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid	tsum iSup ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice Encodable.decode₂ SummationFilter.unconditional	—	tsum_extend_zero Encodable.encode_injective tsum_congr em iSup_congr_Prop Encodable.decode₂_encode iSup_iSup_eq_right Function.Injective.extend_apply Function.extend_apply' Encodable.decode₂_ne_none_iff iSup_neg iSup_bot
tsum_iUnion_decode₂ 📖	mathematical	Set Set.instEmptyCollection AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid	tsum Set.iUnion Encodable.decode₂ SummationFilter.unconditional	—	tsum_iSup_decode₂
tsum_int_eq_zero_add_tsum_pnat 📖	mathematical	Summable AddCommGroup.toAddCommMonoid UniformSpace.toTopologicalSpace SummationFilter.unconditional	tsum AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup PNat PNat.val	—	summable_int_iff_summable_nat_and_neg summable_pnat_iff_summable_succ summable_nat_add_iff IsUniformAddGroup.to_topologicalAddGroup tsum_nat_add_neg IsTopologicalAddGroup.toContinuousAdd tsum_zero_pnat_eq_tsum_nat Summable.add Nat.cast_zero neg_zero add_comm add_assoc AddLeftCancelSemigroup.toIsLeftCancelAdd Summable.tsum_add SummationFilter.instNeBotUnconditional
tsum_int_eq_zero_add_two_mul_tsum_pnat 📖	mathematical	Function.Even Summable AddCommGroup.toAddCommMonoid UniformSpace.toTopologicalSpace SummationFilter.unconditional	tsum AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup AddMonoid.toNatSMul PNat PNat.val	—	two_nsmul add_assoc tsum_int_eq_zero_add_tsum_pnat
tsum_int_rec 📖	mathematical	Summable SummationFilter.unconditional	tsum AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid	—	HasSum.tsum_eq SummationFilter.instNeBotUnconditional Summable.hasSum
tsum_nat_add_neg 📖	mathematical	Summable SummationFilter.unconditional	tsum AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid	—	HasSum.tsum_eq SummationFilter.instNeBotUnconditional HasSum.nat_add_neg Summable.hasSum
tsum_nat_add_neg_add_one 📖	mathematical	Summable SummationFilter.unconditional	tsum AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid	—	HasSum.tsum_eq SummationFilter.instNeBotUnconditional HasSum.nat_add_neg_add_one Summable.hasSum
tsum_of_add_one_of_neg_add_one 📖	mathematical	Summable SummationFilter.unconditional	tsum AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid	—	HasSum.tsum_eq SummationFilter.instNeBotUnconditional HasSum.of_add_one_of_neg_add_one Summable.hasSum
tsum_of_nat_of_neg_add_one 📖	mathematical	Summable SummationFilter.unconditional	tsum AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid	—	HasSum.tsum_eq SummationFilter.instNeBotUnconditional HasSum.of_nat_of_neg_add_one Summable.hasSum
tsum_pnat_eq_tsum_succ 📖	mathematical	—	tsum PNat PNat.val SummationFilter.unconditional	—	Equiv.tsum_eq
tsum_zero_pnat_eq_tsum_nat 📖	mathematical	Summable AddCommGroup.toAddCommMonoid SummationFilter.unconditional	AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup tsum PNat PNat.val	—	Summable.tsum_eq_zero_add AddLeftCancelSemigroup.toIsLeftCancelAdd tsum_pnat_eq_tsum_succ

---

← Back to Index