Documentation Verification Report

Summable

📁 Source: Mathlib/Analysis/SpecialFunctions/Log/Summable.lean

Statistics

Metric	Count
Definitions	0
Theorems `cexp_tsum_eq_tprod`, `hasProd_of_hasSum_log`, `multipliable_of_summable_log`, `multipliable_one_add_of_summable`, `summable_log_one_add_of_summable`, `norm_prod_one_add_sub_one_le`, `eventually_bounded_finset_prod`, `hasProd_of_hasSum_log`, `multipliable_of_summable_log`, `multipliable_of_summable_log'`, `multipliable_one_add_of_summable`, `rexp_tsum_eq_tprod`, `summable_log_one_add_of_summable`, `summable_log_norm_one_add`, `multipliable_norm_one_add_of_summable_norm`, `multipliable_one_add_of_summable`, `prod_vanishing_of_summable_norm`, `tprod_one_add_ne_zero_of_summable`	18
Total	18

Complex

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`cexp_tsum_eq_tprod` 📖	mathematical	`Summable` `Complex` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `instNormedField` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `instNormedAddCommGroup` `log` `SummationFilter.unconditional`	`exp` `tsum` `tprod` `CommRing.toCommMonoid` `commRing`	—	`HasProd.tprod_eq` `instT2Space` `SummationFilter.instNeBotUnconditional` `hasProd_of_hasSum_log` `Summable.hasSum`
`hasProd_of_hasSum_log` 📖	mathematical	`HasSum` `Complex` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `instNormedField` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `instNormedAddCommGroup` `log` `SummationFilter.unconditional`	`HasProd` `CommRing.toCommMonoid` `commRing` `exp`	—	`Filter.Tendsto.congr` `Finset.prod_congr` `exp_log` `HasSum.cexp`
`multipliable_of_summable_log` 📖	mathematical	`Summable` `Complex` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `instNormedField` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `instNormedAddCommGroup` `log` `SummationFilter.unconditional`	`Multipliable` `CommRing.toCommMonoid` `commRing`	—	`multipliable_of_exists_eq_zero` `SummationFilter.instLeAtTopUnconditional` `hasProd_of_hasSum_log` `Summable.hasSum`
`multipliable_one_add_of_summable` 📖	mathematical	`Summable` `Complex` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `instNormedField` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `instNormedAddCommGroup` `SummationFilter.unconditional`	`Multipliable` `CommRing.toCommMonoid` `commRing` `instAdd` `instOne`	—	`multipliable_of_summable_log` `summable_log_one_add_of_summable`
`summable_log_one_add_of_summable` 📖	mathematical	`Summable` `Complex` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `instNormedField` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `instNormedAddCommGroup` `SummationFilter.unconditional`	`log` `instAdd` `instOne`	—	`Summable.of_norm_bounded_eventually` `instCompleteSpace` `Nat.instAtLeastTwoHAddOfNat` `Summable.mul_left` `IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal` `Summable.norm` `FiniteDimensional.rclike_to_real` `Filter.mp_mem` `Filter.Tendsto.eventually_le_const` `instClosedIciTopology` `HasSolidNorm.orderClosedTopology` `instHasSolidNormReal` `Real.instIsOrderedAddMonoid` `one_half_pos` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing` `Summable.tendsto_cofinite_zero` `instIsTopologicalAddGroupReal` `Filter.univ_mem'` `norm_log_one_add_half_le_self`

Finset

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`norm_prod_one_add_sub_one_le` 📖	mathematical	—	`Real` `Real.instLE` `Norm.norm` `NormedRing.toNorm` `NormedCommRing.toNormedRing` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `prod` `CommRing.toCommMonoid` `NormedCommRing.toCommRing` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `NormedRing.toRing` `Real.instSub` `Real.exp` `sum` `Real.instAddCommMonoid` `Real.instOne`	—	`induction_on` `sub_self` `norm_zero` `Real.exp_zero` `prod_insert` `sum_insert` `Real.exp_add` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.sub_congr` `Mathlib.Tactic.Ring.mul_congr` `Mathlib.Tactic.Ring.add_congr` `Mathlib.Tactic.Ring.cast_pos` `Mathlib.Meta.NormNum.isNat_ofNat` `Nat.cast_one` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.add_pf_add_lt` `Mathlib.Tactic.Ring.add_pf_zero_add` `Mathlib.Tactic.Ring.add_mul` `Mathlib.Tactic.Ring.mul_add` `Mathlib.Tactic.Ring.mul_pf_right` `Mathlib.Tactic.Ring.one_mul` `Mathlib.Tactic.Ring.mul_zero` `Mathlib.Tactic.Ring.add_pf_add_zero` `Mathlib.Tactic.Ring.mul_pf_left` `Mathlib.Tactic.Ring.zero_mul` `Mathlib.Tactic.Ring.add_pf_add_gt` `Mathlib.Tactic.Ring.sub_pf` `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` `LE.le.trans` `norm_add_le_of_le` `norm_mul_le` `sub_add_eq_add_sub` `sub_le_sub_iff_right` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `le_imp_le_of_le_of_le` `add_le_add_right` `mul_le_mul_of_nonneg_left` `IsOrderedRing.toPosMulMono` `Real.instIsOrderedRing` `norm_le_norm_sub_add` `norm_nonneg` `le_refl` `add_le_add_left` `NormOneClass.norm_one` `sub_add_cancel` `one_add_mul` `Distrib.rightDistribClass` `add_comm` `mul_le_mul_of_nonneg_right` `IsOrderedRing.toMulPosMono` `Real.add_one_le_exp` `Real.exp_nonneg`

Multipliable

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`eventually_bounded_finset_prod` 📖	mathematical	`Multipliable` `Real` `Real.instCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `SummationFilter.unconditional`	`Real.instLT` `Real.instZero` `Real.instLE` `Finset.prod`	—	`NoMaxOrder.exists_gt` `instNoMaxOrderOfNontrivial` `Real.instIsOrderedRing` `Real.instNontrivial` `Filter.Tendsto.eventually_le_const` `instClosedIciTopology` `HasSolidNorm.orderClosedTopology` `instHasSolidNormReal` `Real.instIsOrderedAddMonoid` `max_lt_iff` `hasProd` `Filter.eventually_atTop` `Finset.isDirected_le` `SummationFilter.unconditional.eq_1`

Real

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`hasProd_of_hasSum_log` 📖	mathematical	`Real` `instLT` `instZero` `HasSum` `instAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `pseudoMetricSpace` `log` `SummationFilter.unconditional`	`HasProd` `instCommMonoid` `exp`	—	`Filter.Tendsto.congr` `Finset.prod_congr` `exp_log` `HasSum.rexp`
`multipliable_of_summable_log` 📖	mathematical	`Real` `instLT` `instZero` `Summable` `instAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `pseudoMetricSpace` `log` `SummationFilter.unconditional`	`Multipliable` `instCommMonoid`	—	`hasProd_of_hasSum_log` `Summable.hasSum`
`multipliable_of_summable_log'` 📖	mathematical	`Summable` `Real` `instAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `pseudoMetricSpace` `log` `SummationFilter.unconditional`	`Multipliable` `instCommMonoid`	—	`Summable.congr_cofinite` `instIsTopologicalAddGroupReal` `Filter.mp_mem` `Filter.univ_mem'` `multipliable_of_summable_log` `instZeroLEOneClass` `NeZero.charZero_one` `RCLike.charZero_rclike` `Multipliable.congr_cofinite₀` `IsTopologicalSemiring.toContinuousMul` `IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal`
`multipliable_one_add_of_summable` 📖	mathematical	`Summable` `Real` `instAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `pseudoMetricSpace` `SummationFilter.unconditional`	`Multipliable` `instCommMonoid` `instAdd` `instOne`	—	`multipliable_of_summable_log'` `Filter.mp_mem` `Filter.Tendsto.eventually_const_lt` `instClosedIicTopology` `HasSolidNorm.orderClosedTopology` `instHasSolidNormReal` `instIsOrderedAddMonoid` `neg_one_lt_zero` `instZeroLEOneClass` `NeZero.charZero_one` `RCLike.charZero_rclike` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `IsOrderedAddMonoid.toAddLeftMono` `Summable.tendsto_cofinite_zero` `instIsTopologicalAddGroupReal` `Filter.univ_mem'` `lt_of_not_ge` `Mathlib.Tactic.Linarith.lt_irrefl` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.add_congr` `Mathlib.Tactic.Ring.sub_congr` `Mathlib.Tactic.Ring.neg_congr` `Mathlib.Tactic.Ring.cast_pos` `Mathlib.Meta.NormNum.isNat_ofNat` `Nat.cast_one` `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.sub_pf` `Mathlib.Tactic.Ring.neg_mul` `Mathlib.Tactic.Ring.add_pf_add_lt` `Mathlib.Tactic.Ring.add_pf_zero_add` `Mathlib.Tactic.Ring.cast_zero` `Nat.cast_zero` `Mathlib.Tactic.Ring.add_pf_add_zero` `Mathlib.Tactic.Ring.add_pf_add_overlap_zero` `Mathlib.Meta.NormNum.IsInt.to_isNat` `Mathlib.Meta.NormNum.isInt_add` `Mathlib.Tactic.Ring.add_overlap_pf_zero` `Mathlib.Tactic.Linarith.add_lt_of_neg_of_le` `instIsStrictOrderedRing` `Mathlib.Tactic.Linarith.sub_neg_of_lt` `instIsOrderedRing` `Mathlib.Tactic.Linarith.sub_nonpos_of_le` `summable_log_one_add_of_summable`
`rexp_tsum_eq_tprod` 📖	mathematical	`Real` `instLT` `instZero` `Summable` `instAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `pseudoMetricSpace` `log` `SummationFilter.unconditional`	`exp` `tsum` `tprod` `instCommMonoid`	—	`HasProd.tprod_eq` `TopologicalSpace.t2Space_of_metrizableSpace` `EMetricSpace.metrizableSpace` `SummationFilter.instNeBotUnconditional` `hasProd_of_hasSum_log` `Summable.hasSum`
`summable_log_one_add_of_summable` 📖	mathematical	`Summable` `Real` `instAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `pseudoMetricSpace` `SummationFilter.unconditional`	`log` `instAdd` `instOne`	—	`Complex.summable_ofReal` `Summable.congr_cofinite` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `Complex.summable_log_one_add_of_summable` `Filter.mp_mem` `Filter.Tendsto.eventually_const_le` `instClosedIicTopology` `HasSolidNorm.orderClosedTopology` `instHasSolidNormReal` `instIsOrderedAddMonoid` `neg_one_lt_zero` `instZeroLEOneClass` `NeZero.charZero_one` `RCLike.charZero_rclike` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `IsOrderedAddMonoid.toAddLeftMono` `Summable.tendsto_cofinite_zero` `instIsTopologicalAddGroupReal` `Filter.univ_mem'` `Complex.ofReal_log` `le_of_not_gt` `Mathlib.Tactic.Linarith.lt_irrefl` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.add_congr` `Mathlib.Tactic.Ring.sub_congr` `Mathlib.Tactic.Ring.neg_congr` `Mathlib.Tactic.Ring.cast_pos` `Mathlib.Meta.NormNum.isNat_ofNat` `Nat.cast_one` `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.sub_pf` `Mathlib.Tactic.Ring.neg_mul` `Mathlib.Tactic.Ring.add_pf_add_lt` `Mathlib.Tactic.Ring.add_pf_zero_add` `Mathlib.Tactic.Ring.cast_zero` `Nat.cast_zero` `Mathlib.Tactic.Ring.add_pf_add_zero` `Mathlib.Tactic.Ring.add_pf_add_overlap_zero` `Mathlib.Meta.NormNum.IsInt.to_isNat` `Mathlib.Meta.NormNum.isInt_add` `Mathlib.Tactic.Ring.add_overlap_pf_zero` `Mathlib.Tactic.Linarith.add_lt_of_le_of_neg` `instIsStrictOrderedRing` `Mathlib.Tactic.Linarith.sub_nonpos_of_le` `instIsOrderedRing` `Mathlib.Tactic.Linarith.sub_neg_of_lt` `Complex.ofReal_add` `Complex.ofReal_one`

Summable

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`summable_log_norm_one_add` 📖	mathematical	`Summable` `Real` `Real.instAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `Norm.norm` `NormedRing.toNorm` `NormedCommRing.toNormedRing` `SummationFilter.unconditional`	`Real.log` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `NormedRing.toRing`	—	`of_norm` `Real.instCompleteSpace` `of_nonneg_of_le` `norm_nonneg` `Real.instIsOrderedAddMonoid` `IsOrderedAddMonoid.toAddLeftMono` `add_neg_cancel_right` `NormOneClass.norm_one` `norm_neg` `norm_add_le` `add_comm` `AddGroup.toOrderedSub` `covariant_swap_add_of_covariant_add` `congr` `Real.summable_log_one_add_of_summable` `add_sub_cancel`

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`multipliable_norm_one_add_of_summable_norm` 📖	mathematical	`Summable` `Real` `Real.instAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `Norm.norm` `NormedRing.toNorm` `NormedCommRing.toNormedRing` `SummationFilter.unconditional`	`Multipliable` `Real.instCommMonoid` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `NormedRing.toRing`	—	`sub_add_cancel` `add_comm` `Real.multipliable_one_add_of_summable` `Summable.of_norm_bounded` `Real.instCompleteSpace` `NormOneClass.norm_one` `add_sub_cancel_left` `abs_norm_sub_norm_le`
`multipliable_one_add_of_summable` 📖	mathematical	`Summable` `Real` `Real.instAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `Norm.norm` `NormedRing.toNorm` `NormedCommRing.toNormedRing` `SummationFilter.unconditional`	`Multipliable` `CommRing.toCommMonoid` `NormedCommRing.toCommRing` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `NormedRing.toRing`	—	`CompleteSpace.complete` `Metric.cauchy_iff` `Filter.map_neBot` `SummationFilter.instNeBotFinsetFilterOfNeBot` `SummationFilter.instNeBotUnconditional` `Multipliable.eventually_bounded_finset_prod` `multipliable_norm_one_add_of_summable_norm` `Nat.instAtLeastTwoHAddOfNat` `prod_vanishing_of_summable_norm` `div_pos` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing` `mul_pos` `Mathlib.Meta.Positivity.pos_of_isNat` `Real.instIsOrderedRing` `Real.instNontrivial` `Mathlib.Meta.NormNum.isNat_ofNat` `Mathlib.Meta.NormNum.instAtLeastTwo` `Finset.prod_congr` `Finset.isDirected_le` `Finset.union_sdiff_of_subset` `Finset.prod_union` `Disjoint.symm` `Finset.sdiff_disjoint` `Metric.mem_ball` `dist_eq_norm_sub` `mul_sub_one` `Mathlib.Tactic.FieldSimp.eq_eq_cancel_eq` `IsCancelMulZero.toIsLeftCancelMulZero` `instIsCancelMulZero` `Mathlib.Tactic.FieldSimp.eq_mul_of_eq_eq_eq_mul` `Mathlib.Tactic.FieldSimp.NF.div_eq_eval` `Mathlib.Tactic.FieldSimp.NF.atom_eq_eval` `Mathlib.Tactic.FieldSimp.NF.div_eq_eval₃` `div_one` `Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval` `one_mul` `Mathlib.Tactic.FieldSimp.eq_div_of_eq_one_of_subst` `Mathlib.Tactic.FieldSimp.NF.mul_eq_eval` `Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₃` `mul_one` `Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₂` `Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons_zero` `Mathlib.Tactic.FieldSimp.NF.eval_cons_of_pow_eq_zero` `ne_of_gt` `Mathlib.Tactic.FieldSimp.NF.cons_ne_zero` `Mathlib.Meta.NormNum.isNat_eq_false` `RCLike.charZero_rclike` `Nat.cast_zero` `one_ne_zero` `NeZero.one` `GroupWithZero.toNontrivial` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.cast_pos` `Nat.cast_one` `LE.le.trans_lt` `norm_mul_le` `lt_of_le_of_lt` `mul_le_mul_of_nonneg_right` `IsOrderedRing.toMulPosMono` `LE.le.trans` `Finset.norm_prod_le` `Finset.subset_union_left` `norm_nonneg` `mul_lt_mul_of_pos_left` `Finset.sdiff_union_distrib` `Finset.inter_assoc` `Finset.sdiff_inter_self` `Finset.inter_empty` `dist_triangle_right` `add_lt_add` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `IsRightCancelAdd.addRightStrictMono_of_addRightMono` `AddRightCancelSemigroup.toIsRightCancelAdd` `covariant_swap_add_of_covariant_add` `add_halves` `CharZero.NeZero.two`
`prod_vanishing_of_summable_norm` 📖	mathematical	`Summable` `Real` `Real.instAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `Norm.norm` `NormedRing.toNorm` `NormedCommRing.toNormedRing` `SummationFilter.unconditional` `Real.instLT` `Real.instZero`	`SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `Finset.prod` `CommRing.toCommMonoid` `NormedCommRing.toCommRing` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `NormedRing.toRing`	—	`Real.exp_zero` `sub_self` `Iio_mem_nhds` `instClosedIciTopology` `HasSolidNorm.orderClosedTopology` `instHasSolidNormReal` `Real.instIsOrderedAddMonoid` `ContinuousAt.preimage_mem_nhds` `ContinuousAt.sub` `IsTopologicalAddGroup.to_continuousSub` `instIsTopologicalAddGroupReal` `ContinuousAt.rexp` `continuousAt_id'` `continuousAt_const` `Summable.vanishing` `LE.le.trans_lt` `Finset.norm_prod_one_add_sub_one_le`
`tprod_one_add_ne_zero_of_summable` 📖	—	`Summable` `Real` `Real.instAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `Norm.norm` `NormedRing.toNorm` `NormedCommRing.toNormedRing` `SummationFilter.unconditional`	—	—	`norm_ne_zero_iff` `Multipliable.norm_tprod` `multipliable_one_add_of_summable` `Real.rexp_tsum_eq_tprod` `norm_pos_iff` `Summable.summable_log_norm_one_add` `Real.exp_ne_zero`

---

← Back to Index