ConditionalInt

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

Statistics

Metric	Count
Definitions `symmetricIcc`, `symmetricIco`, `symmetricIoc`, `symmetricIoo`	4
Theorems `hasProd_symmetricIco_of_hasProd_symmetricIcc`, `hasSum_symmetricIco_of_hasSum_symmetricIcc`, `tendsto_zero_of_even_summable_symmetricIcc`, `hasProd_symmetricIco_of_hasProd_symmetricIcc`, `hasProd_symmetricIcc_iff`, `hasProd_symmetricIco_int_iff`, `hasProd_symmetricIoc_int_iff`, `hasSum_symmetricIcc_iff`, `hasSum_symmetricIco_int_iff`, `hasSum_symmetricIoc_int_iff`, `instLeAtTopSymmetricIcc`, `instLeAtTopSymmetricIco`, `instLeAtTopSymmetricIoc`, `instLeAtTopSymmetricIoo`, `instNeBotSymmetricIcc`, `instNeBotSymmetricIco`, `instNeBotSymmetricIoc`, `instNeBotSymmetricIoo`, `multipliable_symmetricIco_of_multipliable_symmetricIcc`, `multipliable_symmetricIco_of_multiplible_symmetricIcc`, `summable_symmetricIco_of_summable_symmetricIcc`, `symmetricIcc_eq_map_Icc_nat`, `symmetricIcc_eq_symmetricIoo_int`, `symmetricIcc_filter`, `symmetricIcc_le_Conditional`, `symmetricIco_filter`, `symmetricIoc_filter`, `symmetricIoo_filter`, `tprod_symmetricIcc_eq_tprod_symmetricIco`, `tsum_symmetricIcc_eq_tsum_symmetricIco`	30
Total	34

HasProd

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`hasProd_symmetricIco_of_hasProd_symmetricIcc` 📖	mathematical	`HasProd` `CommGroup.toCommMonoid` `SummationFilter.symmetricIcc` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `instConditionallyCompleteLinearOrder` `Int.instLocallyFiniteOrder` `Filter.Tendsto` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `DivisionCommMonoid.toDivisionMonoid` `CommGroup.toDivisionCommMonoid` `Filter.atTop` `Nat.instPreorder` `nhds` `InvOneClass.toOne`	`SummationFilter.symmetricIco`	—	`Filter.tendsto_of_div_tendsto_one` `SummationFilter.symmetricIcc_eq_map_Icc_nat` `Finset.prod_Icc_eq_prod_Ico_mul` `div_mul_cancel_left`

HasSum

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`hasSum_symmetricIco_of_hasSum_symmetricIcc` 📖	mathematical	`HasSum` `AddCommGroup.toAddCommMonoid` `SummationFilter.symmetricIcc` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `instConditionallyCompleteLinearOrder` `Int.instLocallyFiniteOrder` `Filter.Tendsto` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Filter.atTop` `Nat.instPreorder` `nhds` `NegZeroClass.toZero`	`SummationFilter.symmetricIco`	—	`Nat.map_cast_int_atTop` `Filter.tendsto_map'_iff` `Filter.tendsto_of_sub_tendsto_zero` `SummationFilter.symmetricIcc_eq_map_Icc_nat` `Finset.sum_Icc_eq_sum_Ico_add` `sub_add_cancel_left`

Summable

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`tendsto_zero_of_even_summable_symmetricIcc` 📖	mathematical	`Summable` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `SummationFilter.symmetricIcc` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `instConditionallyCompleteLinearOrder` `Int.instLocallyFiniteOrder` `Function.Even`	`Filter.Tendsto` `Filter.atTop` `nhds` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup`	—	`tendsto_zero_iff_norm_tendsto_zero` `Filter.Tendsto.sub` `IsTopologicalAddGroup.to_continuousSub` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `Filter.tendsto_map'_iff` `SummationFilter.symmetricIcc_filter` `HasSum.eq_1` `Filter.Tendsto.comp` `Filter.tendsto_atTop_add_const_right` `Int.instIsOrderedAddMonoid` `Filter.tendsto_id` `Filter.Tendsto.congr'` `Nat.instAtLeastTwoHAddOfNat` `Filter.mp_mem` `Filter.eventually_ge_atTop` `Filter.univ_mem'` `CanLift.prf` `instCanLiftIntNatCastLeOfNat` `le_of_lt` `lt_of_lt_of_le` `Mathlib.Meta.Positivity.pos_of_isNat` `IsStrictOrderedRing.toIsOrderedRing` `Int.instIsStrictOrderedRing` `Int.instNontrivial` `Mathlib.Meta.NormNum.isNat_ofNat` `Finset.Icc_succ_succ` `Finset.sum_union` `Finset.sum_insert` `Finset.sum_singleton` `add_comm` `add_sub_cancel_right` `two_zsmul` `norm_smul` `Int.norm_eq_abs` `Int.cast_two` `abs_two` `Real.instIsOrderedRing` `inv_mul_cancel_left₀` `two_ne_zero` `ZeroLEOneClass.neZero.two` `Real.instZeroLEOneClass` `NeZero.charZero_one` `IsStrictOrderedRing.toCharZero` `Real.instIsStrictOrderedRing` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `Filter.Tendsto.const_mul` `IsTopologicalSemiring.toContinuousMul` `IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal` `sub_self` `MulZeroClass.mul_zero`

SummationFilter

Definitions

Name	Category	Theorems
`symmetricIcc` 📖	CompOp	10 math math: `EisensteinSeries.hasSum_e2Summand_symmetricIcc`, `hasSum_symmetricIcc_iff`, `symmetricIcc_le_Conditional`, `instLeAtTopSymmetricIcc`, `symmetricIcc_filter`, `symmetricIcc_eq_symmetricIoo_int`, `EisensteinSeries.summable_e2Summand_symmetricIcc`, `instNeBotSymmetricIcc`, `symmetricIcc_eq_map_Icc_nat`, `hasProd_symmetricIcc_iff`
`symmetricIco` 📖	CompOp	20 math math: `summable_symmetricIco_of_summable_symmetricIcc`, `tsum_symmetricIcc_eq_tsum_symmetricIco`, `HasProd.hasProd_symmetricIco_of_hasProd_symmetricIcc`, `instLeAtTopSymmetricIco`, `EisensteinSeries.tsum_symmetricIco_linear_sub_linear_add_one_eq_zero`, `EisensteinSeries.G2_eq_tsum_symmetricIco`, `multipliable_symmetricIco_of_multipliable_symmetricIcc`, `symmetricIco_filter`, `EisensteinSeries.hasSum_e2Summand_symmetricIco`, `HasSum.hasSum_symmetricIco_of_hasSum_symmetricIcc`, `multipliable_symmetricIco_of_multiplible_symmetricIcc`, `instNeBotSymmetricIco`, `hasProd_symmetricIco_int_iff`, `hasSum_symmetricIco_int_iff`, `tprod_symmetricIcc_eq_tprod_symmetricIco`, `EisensteinSeries.tsum_tsum_symmetricIco_sub_eq`, `HasProd.hasProd_symmetricIco_of_hasProd_symmetricIcc`, `EisensteinSeries.summable_e2Summand_symmetricIco`, `EisensteinSeries.tsum_symmetricIco_tsum_eq_S_act`, `EisensteinSeries.tsum_symmetricIco_tsum_sub_eq`
`symmetricIoc` 📖	CompOp	5 math math: `hasSum_symmetricIoc_int_iff`, `symmetricIoc_filter`, `instLeAtTopSymmetricIoc`, `hasProd_symmetricIoc_int_iff`, `instNeBotSymmetricIoc`
`symmetricIoo` 📖	CompOp	4 math math: `instLeAtTopSymmetricIoo`, `instNeBotSymmetricIoo`, `symmetricIoo_filter`, `symmetricIcc_eq_symmetricIoo_int`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`hasProd_symmetricIcc_iff` 📖	mathematical	—	`HasProd` `symmetricIcc` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `instConditionallyCompleteLinearOrder` `Int.instLocallyFiniteOrder` `Filter.Tendsto` `Finset.prod` `Finset.Icc` `Filter.atTop` `Nat.instPreorder` `nhds`	—	`Filter.map_map`
`hasProd_symmetricIco_int_iff` 📖	mathematical	—	`HasProd` `symmetricIco` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `instConditionallyCompleteLinearOrder` `Int.instLocallyFiniteOrder` `Filter.Tendsto` `Finset.prod` `Finset.Ico` `Filter.atTop` `Nat.instPreorder` `nhds`	—	`Filter.map_map`
`hasProd_symmetricIoc_int_iff` 📖	mathematical	—	`HasProd` `symmetricIoc` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `instConditionallyCompleteLinearOrder` `Int.instLocallyFiniteOrder` `Filter.Tendsto` `Finset.prod` `Finset.Ioc` `Filter.atTop` `Nat.instPreorder` `nhds`	—	`Filter.map_map`
`hasSum_symmetricIcc_iff` 📖	mathematical	—	`HasSum` `symmetricIcc` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `instConditionallyCompleteLinearOrder` `Int.instLocallyFiniteOrder` `Filter.Tendsto` `Finset.sum` `Finset.Icc` `Filter.atTop` `Nat.instPreorder` `nhds`	—	`Nat.map_cast_int_atTop` `Filter.map_map` `Filter.tendsto_map'_iff`
`hasSum_symmetricIco_int_iff` 📖	mathematical	—	`HasSum` `symmetricIco` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `instConditionallyCompleteLinearOrder` `Int.instLocallyFiniteOrder` `Filter.Tendsto` `Finset.sum` `Finset.Ico` `Filter.atTop` `Nat.instPreorder` `nhds`	—	`Nat.map_cast_int_atTop` `Filter.map_map` `Filter.tendsto_map'_iff`
`hasSum_symmetricIoc_int_iff` 📖	mathematical	—	`HasSum` `symmetricIoc` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `instConditionallyCompleteLinearOrder` `Int.instLocallyFiniteOrder` `Filter.Tendsto` `Finset.sum` `Finset.Ioc` `Filter.atTop` `Nat.instPreorder` `nhds`	—	`Nat.map_cast_int_atTop` `Filter.map_map` `Filter.tendsto_map'_iff`
`instLeAtTopSymmetricIcc` 📖	mathematical	—	`LeAtTop` `symmetricIcc` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `PartialOrder.toPreorder`	—	`le_trans` `symmetricIcc_le_Conditional` `LeAtTop.le_atTop` `instLeAtTopConditional`
`instLeAtTopSymmetricIco` 📖	mathematical	—	`LeAtTop` `symmetricIco` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `PartialOrder.toPreorder`	—	`symmetricIco.eq_1` `Filter.map_le_iff_le_comap` `Filter.tendsto_iff_comap` `Finset.tendsto_Ico_neg_atTop_atTop`
`instLeAtTopSymmetricIoc` 📖	mathematical	—	`LeAtTop` `symmetricIoc` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `PartialOrder.toPreorder`	—	`symmetricIoc.eq_1` `Filter.map_le_iff_le_comap` `Filter.tendsto_iff_comap` `Finset.tendsto_Ioc_neg_atTop_atTop`
`instLeAtTopSymmetricIoo` 📖	mathematical	—	`LeAtTop` `symmetricIoo` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `PartialOrder.toPreorder`	—	`symmetricIoo.eq_1` `Filter.map_le_iff_le_comap` `Filter.tendsto_iff_comap` `Finset.tendsto_Ioo_neg_atTop_atTop`
`instNeBotSymmetricIcc` 📖	mathematical	—	`NeBot` `symmetricIcc`	—	—
`instNeBotSymmetricIco` 📖	mathematical	—	`NeBot` `symmetricIco`	—	—
`instNeBotSymmetricIoc` 📖	mathematical	—	`NeBot` `symmetricIoc`	—	—
`instNeBotSymmetricIoo` 📖	mathematical	—	`NeBot` `symmetricIoo`	—	—
`multipliable_symmetricIco_of_multipliable_symmetricIcc` 📖	mathematical	`Multipliable` `CommGroup.toCommMonoid` `symmetricIcc` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `instConditionallyCompleteLinearOrder` `Int.instLocallyFiniteOrder` `Filter.Tendsto` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `DivisionCommMonoid.toDivisionMonoid` `CommGroup.toDivisionCommMonoid` `Filter.atTop` `Nat.instPreorder` `nhds` `InvOneClass.toOne`	`symmetricIco`	—	`HasProd.multipliable` `HasProd.hasProd_symmetricIco_of_hasProd_symmetricIcc` `Multipliable.hasProd`
`multipliable_symmetricIco_of_multiplible_symmetricIcc` 📖	mathematical	`Multipliable` `CommGroup.toCommMonoid` `symmetricIcc` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `instConditionallyCompleteLinearOrder` `Int.instLocallyFiniteOrder` `Filter.Tendsto` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `DivisionCommMonoid.toDivisionMonoid` `CommGroup.toDivisionCommMonoid` `Filter.atTop` `Nat.instPreorder` `nhds` `InvOneClass.toOne`	`symmetricIco`	—	`multipliable_symmetricIco_of_multipliable_symmetricIcc`
`summable_symmetricIco_of_summable_symmetricIcc` 📖	mathematical	`Summable` `AddCommGroup.toAddCommMonoid` `symmetricIcc` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `instConditionallyCompleteLinearOrder` `Int.instLocallyFiniteOrder` `Filter.Tendsto` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Filter.atTop` `Nat.instPreorder` `nhds` `NegZeroClass.toZero`	`symmetricIco`	—	`HasSum.summable` `HasSum.hasSum_symmetricIco_of_hasSum_symmetricIcc` `Summable.hasSum`
`symmetricIcc_eq_map_Icc_nat` 📖	mathematical	—	`filter` `symmetricIcc` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `instConditionallyCompleteLinearOrder` `Int.instLocallyFiniteOrder` `Filter.map` `Finset` `Finset.Icc` `Filter.atTop` `Nat.instPreorder`	—	`Filter.map_map`
`symmetricIcc_eq_symmetricIoo_int` 📖	mathematical	—	`symmetricIcc` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `instConditionallyCompleteLinearOrder` `Int.instLocallyFiniteOrder` `symmetricIoo`	—	`Filter.ext` `Filter.map_map` `instIsDirectedOrder` `IsStrictOrderedRing.toIsOrderedRing` `Nat.instIsStrictOrderedRing` `instArchimedeanNat` `Nat.cast_add` `Nat.cast_one` `neg_add_rev` `IsRightCancelAdd.addRightStrictMono_of_addRightMono` `AddRightCancelSemigroup.toIsRightCancelAdd` `covariant_swap_add_of_covariant_add` `Int.instAddLeftMono`
`symmetricIcc_filter` 📖	mathematical	—	`filter` `symmetricIcc` `Filter.map` `Finset` `Finset.Icc` `Filter.atTop`	—	—
`symmetricIcc_le_Conditional` 📖	mathematical	—	`Filter` `Finset` `Preorder.toLE` `PartialOrder.toPreorder` `Filter.instPartialOrder` `filter` `symmetricIcc` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `conditional`	—	`Filter.map_mono` `Filter.Tendsto.prodMk` `Filter.tendsto_neg_atTop_atBot` `Filter.tendsto_id`
`symmetricIco_filter` 📖	mathematical	—	`filter` `symmetricIco` `Filter.map` `Finset` `Finset.Ico` `Filter.atTop`	—	—
`symmetricIoc_filter` 📖	mathematical	—	`filter` `symmetricIoc` `Filter.map` `Finset` `Finset.Ioc` `Filter.atTop`	—	—
`symmetricIoo_filter` 📖	mathematical	—	`filter` `symmetricIoo` `Filter.map` `Finset` `Finset.Ioo` `Filter.atTop`	—	—
`tprod_symmetricIcc_eq_tprod_symmetricIco` 📖	mathematical	`Multipliable` `CommGroup.toCommMonoid` `symmetricIcc` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `instConditionallyCompleteLinearOrder` `Int.instLocallyFiniteOrder` `Filter.Tendsto` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `DivisionCommMonoid.toDivisionMonoid` `CommGroup.toDivisionCommMonoid` `Filter.atTop` `Nat.instPreorder` `nhds` `InvOneClass.toOne`	`tprod` `symmetricIco`	—	`HasProd.tprod_eq` `instNeBotSymmetricIco` `Filter.atTop_neBot` `instIsDirectedOrder` `IsStrictOrderedRing.toIsOrderedRing` `Int.instIsStrictOrderedRing` `instArchimedeanInt` `HasProd.hasProd_symmetricIco_of_hasProd_symmetricIcc` `Multipliable.hasProd`
`tsum_symmetricIcc_eq_tsum_symmetricIco` 📖	mathematical	`Summable` `AddCommGroup.toAddCommMonoid` `symmetricIcc` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `instConditionallyCompleteLinearOrder` `Int.instLocallyFiniteOrder` `Filter.Tendsto` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Filter.atTop` `Nat.instPreorder` `nhds` `NegZeroClass.toZero`	`tsum` `symmetricIco`	—	`HasSum.tsum_eq` `instNeBotSymmetricIco` `Filter.atTop_neBot` `instIsDirectedOrder` `IsStrictOrderedRing.toIsOrderedRing` `Int.instIsStrictOrderedRing` `instArchimedeanInt` `HasSum.hasSum_symmetricIco_of_hasSum_symmetricIcc` `Summable.hasSum`

SummationFilter.HasProd

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`hasProd_symmetricIco_of_hasProd_symmetricIcc` 📖	mathematical	`HasProd` `CommGroup.toCommMonoid` `SummationFilter.symmetricIcc` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `instConditionallyCompleteLinearOrder` `Int.instLocallyFiniteOrder` `Filter.Tendsto` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `DivisionCommMonoid.toDivisionMonoid` `CommGroup.toDivisionCommMonoid` `Filter.atTop` `Nat.instPreorder` `nhds` `InvOneClass.toOne`	`SummationFilter.symmetricIco`	—	`HasProd.hasProd_symmetricIco_of_hasProd_symmetricIcc`

---

← Back to Index