Documentation Verification Report

Summable

📁 Source: Mathlib/NumberTheory/ModularForms/EisensteinSeries/E2/Summable.lean

Statistics

Metric	Count
Definitions	0
Theorems `G2_eq_tsum_cexp`, `G2_eq_tsum_symmetricIco`, `hasSum_e2Summand_symmetricIcc`, `hasSum_e2Summand_symmetricIco`, `summable_e2Summand_symmetricIcc`, `summable_e2Summand_symmetricIco`, `summable_left_one_div_linear_sub_one_div_linear`, `summable_right_one_div_linear_sub_one_div_linear_succ`, `tendsto_double_sum_S_act`, `tendsto_e2Summand_atTop_nhds_zero`, `tendsto_tsum_one_div_linear_sub_succ_eq`, `tsum_symmetricIco_linear_sub_linear_add_one_eq_zero`, `tsum_symmetricIco_tsum_eq_S_act`, `tsum_symmetricIco_tsum_sub_eq`, `tsum_tsum_symmetricIco_sub_eq`	15
Total	15

EisensteinSeries

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`G2_eq_tsum_cexp` 📖	mathematical	—	`G2` `Complex` `Complex.instSub` `Complex.instMul` `instOfNatAtLeastTwo` `Complex.instNatCast` `Nat.instAtLeastTwoHAddOfNat` `riemannZeta` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Complex.instSemiring` `Complex.ofReal` `Real.pi` `tsum` `PNat` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `CommCStarAlgebra.toNormedCommRing` `instCommCStarAlgebraComplex` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `Complex.instNormedAddCommGroup` `DFunLike.coe` `ArithmeticFunction` `MulZeroClass.toZero` `Nat.instMulZeroClass` `ArithmeticFunction.instFunLikeNat` `ArithmeticFunction.sigma` `PNat.val` `Complex.exp` `Complex.I` `UpperHalfPlane.coe` `SummationFilter.unconditional`	—	`HasSum.tsum_eq` `Nat.instAtLeastTwoHAddOfNat` `Complex.instT2Space` `SummationFilter.instNeBotSymmetricIcc` `Filter.atTop_neBot` `instIsDirectedOrder` `IsStrictOrderedRing.toIsOrderedRing` `Int.instIsStrictOrderedRing` `instArchimedeanInt` `hasSum_e2Summand_symmetricIcc`
`G2_eq_tsum_symmetricIco` 📖	mathematical	—	`G2` `tsum` `Complex` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `CommCStarAlgebra.toNormedCommRing` `instCommCStarAlgebraComplex` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `Complex.instNormedAddCommGroup` `e2Summand` `SummationFilter.symmetricIco` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `instConditionallyCompleteLinearOrder` `Int.instLocallyFiniteOrder`	—	`G2.eq_1` `SummationFilter.tsum_symmetricIcc_eq_tsum_symmetricIco` `IsTopologicalSemiring.toContinuousAdd` `IsTopologicalRing.toIsTopologicalSemiring` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `Complex.instT2Space` `summable_e2Summand_symmetricIcc` `neg_zero` `Filter.Tendsto.comp` `Filter.Tendsto.neg` `IsTopologicalRing.toContinuousNeg` `tendsto_e2Summand_atTop_nhds_zero` `tendsto_natCast_atTop_atTop` `IsStrictOrderedRing.toIsOrderedRing` `Int.instIsStrictOrderedRing` `instArchimedeanInt`
`hasSum_e2Summand_symmetricIcc` 📖	mathematical	—	`HasSum` `Complex` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `CommCStarAlgebra.toNormedCommRing` `instCommCStarAlgebraComplex` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `Complex.instNormedAddCommGroup` `e2Summand` `Complex.instSub` `Complex.instMul` `instOfNatAtLeastTwo` `Complex.instNatCast` `Nat.instAtLeastTwoHAddOfNat` `riemannZeta` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Complex.instSemiring` `Complex.ofReal` `Real.pi` `tsum` `PNat` `DFunLike.coe` `ArithmeticFunction` `MulZeroClass.toZero` `Nat.instMulZeroClass` `ArithmeticFunction.instFunLikeNat` `ArithmeticFunction.sigma` `PNat.val` `Complex.exp` `Complex.I` `UpperHalfPlane.coe` `SummationFilter.unconditional` `SummationFilter.symmetricIcc` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `instConditionallyCompleteLinearOrder` `Int.instLocallyFiniteOrder`	—	`Nat.instAtLeastTwoHAddOfNat` `Finset.sum_congr` `SummationFilter.symmetricIcc_eq_map_Icc_nat` `neg_mul` `Finset.sum_neg_distrib` `Filter.Tendsto.const_add` `IsTopologicalSemiring.toContinuousAdd` `IsTopologicalRing.toIsTopologicalSemiring` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.to_isTopologicalDivisionRing`
`hasSum_e2Summand_symmetricIco` 📖	mathematical	—	`HasSum` `Complex` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `CommCStarAlgebra.toNormedCommRing` `instCommCStarAlgebraComplex` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `Complex.instNormedAddCommGroup` `e2Summand` `Complex.instSub` `Complex.instMul` `instOfNatAtLeastTwo` `Complex.instNatCast` `Nat.instAtLeastTwoHAddOfNat` `riemannZeta` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Complex.instSemiring` `Complex.ofReal` `Real.pi` `tsum` `PNat` `DFunLike.coe` `ArithmeticFunction` `MulZeroClass.toZero` `Nat.instMulZeroClass` `ArithmeticFunction.instFunLikeNat` `ArithmeticFunction.sigma` `PNat.val` `Complex.exp` `Complex.I` `UpperHalfPlane.coe` `SummationFilter.unconditional` `SummationFilter.symmetricIco` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `instConditionallyCompleteLinearOrder` `Int.instLocallyFiniteOrder`	—	`HasSum.hasSum_symmetricIco_of_hasSum_symmetricIcc` `IsTopologicalSemiring.toContinuousAdd` `IsTopologicalRing.toIsTopologicalSemiring` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `Nat.instAtLeastTwoHAddOfNat` `hasSum_e2Summand_symmetricIcc` `neg_zero` `Filter.Tendsto.comp` `Filter.Tendsto.neg` `IsTopologicalRing.toContinuousNeg` `tendsto_e2Summand_atTop_nhds_zero` `tendsto_natCast_atTop_atTop` `IsStrictOrderedRing.toIsOrderedRing` `Int.instIsStrictOrderedRing` `instArchimedeanInt`
`summable_e2Summand_symmetricIcc` 📖	mathematical	—	`Summable` `Complex` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `CommCStarAlgebra.toNormedCommRing` `instCommCStarAlgebraComplex` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `Complex.instNormedAddCommGroup` `e2Summand` `SummationFilter.symmetricIcc` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `instConditionallyCompleteLinearOrder` `Int.instLocallyFiniteOrder`	—	`HasSum.summable` `Nat.instAtLeastTwoHAddOfNat` `hasSum_e2Summand_symmetricIcc`
`summable_e2Summand_symmetricIco` 📖	mathematical	—	`Summable` `Complex` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `CommCStarAlgebra.toNormedCommRing` `instCommCStarAlgebraComplex` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `Complex.instNormedAddCommGroup` `e2Summand` `SummationFilter.symmetricIco` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `instConditionallyCompleteLinearOrder` `Int.instLocallyFiniteOrder`	—	`HasSum.summable` `Nat.instAtLeastTwoHAddOfNat` `hasSum_e2Summand_symmetricIco`
`summable_left_one_div_linear_sub_one_div_linear` 📖	mathematical	—	`Summable` `Complex` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `CommCStarAlgebra.toNormedCommRing` `instCommCStarAlgebraComplex` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `Complex.instNormedAddCommGroup` `Complex.instSub` `DivInvMonoid.toDiv` `Complex.instDivInvMonoid` `Complex.instOne` `Complex.instAdd` `Complex.instMul` `Complex.instIntCast` `UpperHalfPlane.coe` `SummationFilter.unconditional`	—	`Summable.mul_left` `IsTopologicalRing.toIsTopologicalSemiring` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `summable_linear_left_mul_linear_left` `UpperHalfPlane.ne_zero` `Finset.summable_compl_iff` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `Summable.congr`
`summable_right_one_div_linear_sub_one_div_linear_succ` 📖	mathematical	—	`Summable` `Complex` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `CommCStarAlgebra.toNormedCommRing` `instCommCStarAlgebraComplex` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `Complex.instNormedAddCommGroup` `Complex.instSub` `DivInvMonoid.toDiv` `Complex.instDivInvMonoid` `Complex.instOne` `Complex.instAdd` `Complex.instMul` `Complex.instIntCast` `UpperHalfPlane.coe` `SummationFilter.unconditional`	—	`summable_linear_right_add_one_mul_linear_right` `Finset.summable_compl_iff` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `Summable.congr` `mul_comm` `add_assoc` `mul_inv_rev` `one_div` `Int.cast_add` `Int.cast_one` `add_sub_cancel_left` `one_mul`
`tendsto_double_sum_S_act` 📖	mathematical	—	`Filter.Tendsto` `Complex` `tsum` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `CommCStarAlgebra.toNormedCommRing` `instCommCStarAlgebraComplex` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `Complex.instNormedAddCommGroup` `Finset.sum` `Finset.Ico` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `instConditionallyCompleteLinearOrder` `Int.instLocallyFiniteOrder` `DivInvMonoid.toDiv` `Complex.instDivInvMonoid` `Complex.instOne` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Complex.instSemiring` `Complex.instAdd` `Complex.instMul` `Complex.instIntCast` `UpperHalfPlane.coe` `SummationFilter.unconditional` `Filter.atTop` `Nat.instPreorder` `nhds` `Complex.instInv` `G2` `Matrix.SpecialLinearGroup` `Fin.fintype` `Int.instCommRing` `UpperHalfPlane` `SemigroupAction.toSMul` `Monoid.toSemigroup` `Matrix.SpecialLinearGroup.monoid` `MulAction.toSemigroupAction` `UpperHalfPlane.SLAction` `Ring.toIntAlgebra` `Real` `Real.instRing` `ModularGroup.S`	—	`G2_eq_tsum_symmetricIco` `tsum_mul_left` `IsTopologicalRing.toIsTopologicalSemiring` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `Complex.instT2Space` `Summable.hasSum` `Summable.mul_left` `summable_e2Summand_symmetricIco` `UpperHalfPlane.im_inv_neg_coe_pos` `UpperHalfPlane.modular_S_smul` `Filter.Tendsto.congr` `Finset.sum_congr` `inv_neg` `mul_neg` `Matrix.cons_val_fin_one` `zpow_neg` `one_div`
`tendsto_e2Summand_atTop_nhds_zero` 📖	mathematical	—	`Filter.Tendsto` `Complex` `e2Summand` `Filter.atTop` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `instConditionallyCompleteLinearOrder` `nhds` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `CommCStarAlgebra.toNormedCommRing` `instCommCStarAlgebraComplex` `Complex.instZero`	—	`Summable.tendsto_zero_of_even_summable_symmetricIcc` `RCLike.instNormSMulClassInt` `summable_e2Summand_symmetricIcc` `e2Summand_even`
`tendsto_tsum_one_div_linear_sub_succ_eq` 📖	mathematical	—	`Filter.Tendsto` `PNat` `Complex` `Finset.sum` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `CommCStarAlgebra.toNormedCommRing` `instCommCStarAlgebraComplex` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `Complex.instNormedAddCommGroup` `Finset.Ico` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `instConditionallyCompleteLinearOrder` `Int.instLocallyFiniteOrder` `PNat.val` `tsum` `Complex.instSub` `DivInvMonoid.toDiv` `Complex.instDivInvMonoid` `Complex.instOne` `Complex.instAdd` `Complex.instMul` `Complex.instIntCast` `UpperHalfPlane.coe` `SummationFilter.unconditional` `Filter.atTop` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instLinearOrderPNat` `nhds` `Complex.instNeg` `instOfNatAtLeastTwo` `Complex.instNatCast` `Nat.instAtLeastTwoHAddOfNat` `Complex.ofReal` `Real.pi` `Complex.I`	—	`Summable.tsum_finsetSum` `Complex.instT2Space` `IsTopologicalSemiring.toContinuousAdd` `IsTopologicalRing.toIsTopologicalSemiring` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `SummationFilter.instNeBotUnconditional` `Summable.congr` `summable_left_one_div_linear_sub_one_div_linear` `Nat.instAtLeastTwoHAddOfNat` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.div_congr` `Mathlib.Tactic.Ring.mul_congr` `Mathlib.Tactic.Ring.neg_congr` `Mathlib.Tactic.Ring.cast_pos` `Mathlib.Meta.NormNum.isNat_ofNat` `Mathlib.Meta.NormNum.instAtLeastTwo` `Mathlib.Tactic.Ring.neg_add` `Mathlib.Tactic.Ring.neg_one_mul` `Mathlib.Meta.NormNum.IsInt.to_raw_eq` `Mathlib.Meta.NormNum.isInt_mul` `Mathlib.Meta.NormNum.IsInt.of_raw` `Mathlib.Meta.NormNum.IsNat.to_isInt` `Mathlib.Meta.NormNum.IsNat.of_raw` `Mathlib.Tactic.Ring.neg_zero` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.add_mul` `Mathlib.Tactic.Ring.mul_add` `Mathlib.Tactic.Ring.mul_pf_right` `Mathlib.Tactic.Ring.mul_one` `Mathlib.Tactic.Ring.mul_zero` `Mathlib.Tactic.Ring.add_pf_add_zero` `Mathlib.Tactic.Ring.zero_mul` `Mathlib.Tactic.Ring.mul_pf_left` `Mathlib.Tactic.Ring.div_pf` `Mathlib.Tactic.Ring.inv_single` `Mathlib.Tactic.Ring.inv_mul` `Mathlib.Meta.NormNum.IsNat.to_raw_eq` `Mathlib.Meta.NormNum.IsNNRat.to_isNat` `Mathlib.Meta.NormNum.isNNRat_inv_pos` `Complex.instCharZero` `Mathlib.Meta.NormNum.IsNat.to_isNNRat` `Mathlib.Tactic.Ring.one_mul` `Mathlib.Tactic.Ring.add_congr` `Mathlib.Tactic.Ring.cast_zero` `Nat.cast_zero` `Mathlib.Tactic.Ring.add_pf_zero_add` `Filter.Tendsto.add` `neg_mul` `MulZeroClass.mul_zero` `Filter.Tendsto.const_mul` `IsTopologicalSemiring.toContinuousMul` `tendsto_inv_atTop_nhds_zero_nat` `NNRat.instContinuousSMulOfIsScalarTowerOfRat` `IsScalarTower.nnrat` `Rat.instCharZero` `IsBoundedSMul.continuousSMul` `NormedSpace.toIsBoundedSMul`
`tsum_symmetricIco_linear_sub_linear_add_one_eq_zero` 📖	mathematical	—	`tsum` `Complex` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `CommCStarAlgebra.toNormedCommRing` `instCommCStarAlgebraComplex` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `Complex.instNormedAddCommGroup` `Complex.instSub` `DivInvMonoid.toDiv` `Complex.instDivInvMonoid` `Complex.instOne` `Complex.instAdd` `Complex.instMul` `Complex.instIntCast` `UpperHalfPlane.coe` `SummationFilter.symmetricIco` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `instConditionallyCompleteLinearOrder` `Int.instLocallyFiniteOrder` `Complex.instZero`	—	`HasSum.tsum_eq` `Complex.instT2Space` `SummationFilter.instNeBotSymmetricIco` `Filter.atTop_neBot` `instIsDirectedOrder` `IsStrictOrderedRing.toIsOrderedRing` `Int.instIsStrictOrderedRing` `instArchimedeanInt` `one_div` `sub_self` `Filter.Tendsto.sub` `IsTopologicalAddGroup.to_continuousSub` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `tendsto_zero_inv_linear_sub` `tendsto_zero_inv_linear`
`tsum_symmetricIco_tsum_eq_S_act` 📖	mathematical	—	`tsum` `Complex` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `CommCStarAlgebra.toNormedCommRing` `instCommCStarAlgebraComplex` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `Complex.instNormedAddCommGroup` `DivInvMonoid.toDiv` `Complex.instDivInvMonoid` `Complex.instOne` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Complex.instSemiring` `Complex.instAdd` `Complex.instMul` `Complex.instIntCast` `UpperHalfPlane.coe` `SummationFilter.unconditional` `SummationFilter.symmetricIco` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `instConditionallyCompleteLinearOrder` `Int.instLocallyFiniteOrder` `Complex.instInv` `G2` `Matrix.SpecialLinearGroup` `Fin.fintype` `Int.instCommRing` `UpperHalfPlane` `SemigroupAction.toSMul` `Monoid.toSemigroup` `Matrix.SpecialLinearGroup.monoid` `MulAction.toSemigroupAction` `UpperHalfPlane.SLAction` `Ring.toIntAlgebra` `Real` `Real.instRing` `ModularGroup.S`	—	`HasSum.tsum_eq` `Complex.instT2Space` `SummationFilter.instNeBotSymmetricIco` `Filter.atTop_neBot` `instIsDirectedOrder` `IsStrictOrderedRing.toIsOrderedRing` `Int.instIsStrictOrderedRing` `instArchimedeanInt` `SummationFilter.hasSum_symmetricIco_int_iff` `Filter.Tendsto.congr` `Summable.tsum_finsetSum` `IsTopologicalSemiring.toContinuousAdd` `IsTopologicalRing.toIsTopologicalSemiring` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `SummationFilter.instNeBotUnconditional` `one_div` `linear_left_summable` `UpperHalfPlane.ne_zero` `le_rfl` `tendsto_double_sum_S_act`
`tsum_symmetricIco_tsum_sub_eq` 📖	mathematical	—	`tsum` `Complex` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `CommCStarAlgebra.toNormedCommRing` `instCommCStarAlgebraComplex` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `Complex.instNormedAddCommGroup` `Complex.instSub` `DivInvMonoid.toDiv` `Complex.instDivInvMonoid` `Complex.instOne` `Complex.instAdd` `Complex.instMul` `Complex.instIntCast` `UpperHalfPlane.coe` `SummationFilter.unconditional` `SummationFilter.symmetricIco` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `instConditionallyCompleteLinearOrder` `Int.instLocallyFiniteOrder` `Complex.instNeg` `instOfNatAtLeastTwo` `Complex.instNatCast` `Nat.instAtLeastTwoHAddOfNat` `Complex.ofReal` `Real.pi` `Complex.I`	—	`HasSum.tsum_eq` `Nat.instAtLeastTwoHAddOfNat` `Complex.instT2Space` `SummationFilter.instNeBotSymmetricIco` `Filter.atTop_neBot` `instIsDirectedOrder` `IsStrictOrderedRing.toIsOrderedRing` `Int.instIsStrictOrderedRing` `instArchimedeanInt` `Finset.sum_congr` `one_div` `Filter.map_map` `neg_mul` `tendsto_tsum_one_div_linear_sub_succ_eq`
`tsum_tsum_symmetricIco_sub_eq` 📖	mathematical	—	`tsum` `Complex` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `CommCStarAlgebra.toNormedCommRing` `instCommCStarAlgebraComplex` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `Complex.instNormedAddCommGroup` `Complex.instSub` `DivInvMonoid.toDiv` `Complex.instDivInvMonoid` `Complex.instOne` `Complex.instAdd` `Complex.instMul` `Complex.instIntCast` `UpperHalfPlane.coe` `SummationFilter.symmetricIco` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `instConditionallyCompleteLinearOrder` `Int.instLocallyFiniteOrder` `SummationFilter.unconditional` `Complex.instZero`	—	`tsum_symmetricIco_linear_sub_linear_add_one_eq_zero` `tsum_zero`

---

← Back to Index