PSeries

📁 Source: Mathlib/Analysis/PSeries.lean

Statistics

Metric	Count
Definitions SuccDiffBounded	1
Theorems le_tsum_condensed, le_tsum_schlomilch, tsum_condensed_le, tsum_schlomilch_le, le_sum_condensed, le_sum_condensed', le_sum_schlomilch, le_sum_schlomilch', sum_condensed_le, sum_condensed_le', sum_schlomilch_le, sum_schlomilch_le', summable_condensed_iff, summable_one_div_rpow, summable_rpow, summable_rpow_inv, summable_schlomilch_iff, not_summable_indicator_one_div_natCast, not_summable_natCast_inv, not_summable_one_div_natCast, summable_abs_int_rpow, summable_nat_pow_inv, summable_nat_rpow, summable_nat_rpow_inv, summable_one_div_int_add_rpow, summable_one_div_int_pow, summable_one_div_nat_add_rpow, summable_one_div_nat_pow, summable_one_div_nat_rpow, tendsto_sum_range_one_div_nat_succ_atTop, sum_Ioc_inv_sq_le_sub, sum_Ioo_inv_sq_le, summable_condensed_iff_of_eventually_nonneg, summable_condensed_iff_of_nonneg, summable_pow_div_add, summable_schlomilch_iff_of_nonneg	36
Total	37

ENNReal

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
le_tsum_condensed 📖	mathematical	ENNReal Preorder.toLE PartialOrder.toPreorder instPartialOrder	tsum instAddCommMonoid instTopologicalSpace SummationFilter.unconditional Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring instCommSemiring Distrib.toMul Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero instOfNatAtLeastTwo AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal Nat.instAtLeastTwoHAddOfNat Nat.instMonoid	—	Nat.instAtLeastTwoHAddOfNat tsum_eq_iSup_nat' tendsto_pow_atTop_atTop_of_one_lt Nat.instIsStrictOrderedRing StarOrderedRing.toExistsAddOfLE Nat.instStarOrderedRing instArchimedeanNat one_lt_two Nat.instZeroLEOneClass IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd IsOrderedAddMonoid.toAddLeftMono Nat.instIsOrderedAddMonoid iSup_le LE.le.trans Finset.le_sum_condensed instIsOrderedAddMonoid Finset.sum_congr nsmul_eq_mul Nat.cast_pow le_imp_le_of_le_of_le add_le_add_right sum_le_tsum le_refl
le_tsum_schlomilch 📖	mathematical	ENNReal Preorder.toLE PartialOrder.toPreorder instPartialOrder StrictMono Nat.instPreorder	tsum instAddCommMonoid instTopologicalSpace SummationFilter.unconditional Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring instCommSemiring Finset.sum Finset.range Distrib.toMul instSub AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal	—	tsum_eq_iSup_nat' StrictMono.tendsto_atTop iSup_le le_imp_le_of_le_of_le Finset.le_sum_schlomilch instIsOrderedAddMonoid StrictMono.monotone le_refl add_le_add_right IsOrderedAddMonoid.toAddLeftMono natCast_sub Finset.sum_congr nsmul_eq_mul sum_le_tsum
tsum_condensed_le 📖	mathematical	ENNReal Preorder.toLE PartialOrder.toPreorder instPartialOrder	tsum instAddCommMonoid instTopologicalSpace Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring instCommSemiring Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero instOfNatAtLeastTwo AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal Nat.instAtLeastTwoHAddOfNat Nat.instMonoid SummationFilter.unconditional Distrib.toAdd	—	Nat.instAtLeastTwoHAddOfNat tsum_eq_iSup_nat' Filter.tendsto_atTop_mono Filter.tendsto_id two_mul two_nsmul iSup_le le_imp_le_of_le_of_le le_refl add_le_add_right IsOrderedAddMonoid.toAddLeftMono instIsOrderedAddMonoid smul_le_smul_of_nonneg_left OrderedSemiring.toPosSMulMonoNat instIsOrderedRing sum_le_tsum le_of_lt Mathlib.Meta.Positivity.pos_of_isNat IsStrictOrderedRing.toIsOrderedRing Nat.instIsStrictOrderedRing Nat.instNontrivial Mathlib.Meta.NormNum.isNat_ofNat nsmul_eq_mul Finset.sum_congr Nat.cast_pow Finset.sum_condensed_le
tsum_schlomilch_le 📖	mathematical	ENNReal Preorder.toLE PartialOrder.toPreorder instPartialOrder instZeroENNReal Monotone Nat.instPreorder SuccDiffBounded	tsum instAddCommMonoid instTopologicalSpace Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring instCommSemiring instSub AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal SummationFilter.unconditional Distrib.toAdd	—	tsum_eq_iSup_nat' Filter.tendsto_atTop_mono Filter.tendsto_id iSup_le le_imp_le_of_le_of_le le_refl add_le_add_right IsOrderedAddMonoid.toAddLeftMono instIsOrderedAddMonoid mul_le_mul_right IsOrderedMonoid.toMulLeftMono instIsOrderedMonoid sum_le_tsum Finset.sum_congr nsmul_eq_mul natCast_sub Finset.sum_schlomilch_le

Finset

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
le_sum_condensed 📖	mathematical	Preorder.toLE PartialOrder.toPreorder	sum range Monoid.toNatPow Nat.instMonoid AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddMonoid.toNatSMul AddCommMonoid.toAddMonoid	—	le_imp_le_of_le_of_le le_refl add_le_add_right IsOrderedAddMonoid.toAddLeftMono le_sum_condensed' sum_range_add_sum_Ico sum_range_succ sum_range_zero zero_add
le_sum_condensed' 📖	mathematical	Preorder.toLE PartialOrder.toPreorder	sum Ico Nat.instPreorder Nat.instLocallyFiniteOrder Monoid.toNatPow Nat.instMonoid range AddMonoid.toNatSMul AddCommMonoid.toAddMonoid	—	Nat.instAtLeastTwoHAddOfNat sum_congr pow_succ mul_two add_tsub_cancel_right Nat.instOrderedSub IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT AddLeftCancelSemigroup.toIsLeftCancelAdd contravariant_lt_of_covariant_le IsOrderedAddMonoid.toAddLeftMono Nat.instIsOrderedAddMonoid le_sum_schlomilch' pow_pos LinearOrderedCommMonoidWithZero.toPosMulStrictMono Nat.instZeroLEOneClass zero_lt_two pow_right_mono₀ IsOrderedRing.toPosMulMono IsStrictOrderedRing.toIsOrderedRing Nat.instIsStrictOrderedRing one_le_two
le_sum_schlomilch 📖	mathematical	Preorder.toLE PartialOrder.toPreorder Monotone Nat.instPreorder	sum range AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddMonoid.toNatSMul AddCommMonoid.toAddMonoid	—	le_imp_le_of_le_of_le le_refl add_le_add_right IsOrderedAddMonoid.toAddLeftMono le_sum_schlomilch' sum_range_add_sum_Ico
le_sum_schlomilch' 📖	mathematical	Preorder.toLE PartialOrder.toPreorder Monotone Nat.instPreorder	sum Ico Nat.instLocallyFiniteOrder range AddMonoid.toNatSMul AddCommMonoid.toAddMonoid	—	sum_congr Ico_eq_empty_of_le mem_Ico sum_const Nat.card_Ico sum_le_sum IsOrderedAddMonoid.toAddLeftMono sum_range_succ sum_Ico_consecutive add_le_add covariant_swap_add_of_covariant_add
sum_condensed_le 📖	mathematical	Preorder.toLE PartialOrder.toPreorder	sum range AddMonoid.toNatSMul AddCommMonoid.toAddMonoid Monoid.toNatPow Nat.instMonoid AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup Ico Nat.instPreorder Nat.instLocallyFiniteOrder	—	le_imp_le_of_le_of_le le_refl add_le_add_right IsOrderedAddMonoid.toAddLeftMono smul_le_smul_of_nonneg_left instPosSMulMonoNatOfIsOrderedAddMonoid sum_condensed_le' le_of_lt Mathlib.Meta.Positivity.pos_of_isNat IsStrictOrderedRing.toIsOrderedRing Nat.instIsStrictOrderedRing Nat.instNontrivial Mathlib.Meta.NormNum.isNat_ofNat sum_range_succ' sum_congr pow_succ' mul_nsmul' sum_nsmul pow_zero one_smul add_comm
sum_condensed_le' 📖	mathematical	Preorder.toLE PartialOrder.toPreorder	sum range AddMonoid.toNatSMul AddCommMonoid.toAddMonoid Monoid.toNatPow Nat.instMonoid Ico Nat.instPreorder Nat.instLocallyFiniteOrder	—	Nat.instAtLeastTwoHAddOfNat sum_congr pow_succ mul_two add_tsub_cancel_right Nat.instOrderedSub IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT AddLeftCancelSemigroup.toIsLeftCancelAdd contravariant_lt_of_covariant_le IsOrderedAddMonoid.toAddLeftMono Nat.instIsOrderedAddMonoid sum_schlomilch_le' pow_pos LinearOrderedCommMonoidWithZero.toPosMulStrictMono Nat.instZeroLEOneClass zero_lt_two pow_right_mono₀ IsOrderedRing.toPosMulMono IsStrictOrderedRing.toIsOrderedRing Nat.instIsStrictOrderedRing one_le_two
sum_schlomilch_le 📖	mathematical	Preorder.toLE PartialOrder.toPreorder AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid Monotone Nat.instPreorder SuccDiffBounded	sum range AddMonoid.toNatSMul AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup Ico Nat.instLocallyFiniteOrder	—	sum_range_succ' add_comm add_le_add_right IsOrderedAddMonoid.toAddLeftMono smul_smul smul_le_smul_of_nonneg_right instSMulPosMonoNatOfIsOrderedAddMonoid smul_sum sum_le_sum LE.le.trans nsmul_le_nsmul_right covariant_swap_add_of_covariant_add sum_schlomilch_le'
sum_schlomilch_le' 📖	mathematical	Preorder.toLE PartialOrder.toPreorder Monotone Nat.instPreorder	sum range AddMonoid.toNatSMul AddCommMonoid.toAddMonoid Ico Nat.instLocallyFiniteOrder	—	sum_congr Ico_eq_empty_of_le LT.lt.trans_le le_rfl mem_Ico sum_const Nat.card_Ico sum_le_sum IsOrderedAddMonoid.toAddLeftMono sum_range_succ sum_Ico_consecutive add_le_add_left covariant_swap_add_of_covariant_add Nat.instIsOrderedAddMonoid add_le_add

NNReal

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
summable_condensed_iff 📖	mathematical	NNReal Preorder.toLE PartialOrder.toPreorder instPartialOrderNNReal	Summable NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring instSemiringNNReal instTopologicalSpace Distrib.toMul NonUnitalNonAssocSemiring.toDistrib Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero instOfNatAtLeastTwo AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Nat.instAtLeastTwoHAddOfNat Nat.instMonoid SummationFilter.unconditional	—	pow_succ mul_two add_tsub_cancel_right Nat.instOrderedSub IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT AddLeftCancelSemigroup.toIsLeftCancelAdd contravariant_lt_of_covariant_le IsOrderedAddMonoid.toAddLeftMono Nat.instIsOrderedAddMonoid two_mul Nat.instAtLeastTwoHAddOfNat Nat.cast_add Nat.cast_pow instOrderedSub addLeftReflectLT summable_schlomilch_iff pow_pos LinearOrderedCommMonoidWithZero.toPosMulStrictMono Nat.instZeroLEOneClass zero_lt_two pow_right_strictMono₀ one_lt_two IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono two_ne_zero
summable_one_div_rpow 📖	mathematical	—	Summable NNReal NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring instSemiringNNReal instTopologicalSpace instDiv instOneNNReal Real instPowReal AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne SummationFilter.unconditional Real.instLT Real.instOne	—	one_div
summable_rpow 📖	mathematical	—	Summable NNReal NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring instSemiringNNReal instTopologicalSpace Real instPowReal AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne SummationFilter.unconditional Real.instLT Real.instNeg Real.instOne	—	coe_natCast
summable_rpow_inv 📖	mathematical	—	Summable NNReal NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring instSemiringNNReal instTopologicalSpace instInv Real instPowReal AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne SummationFilter.unconditional Real.instLT Real.instOne	—	coe_natCast
summable_schlomilch_iff 📖	mathematical	NNReal Preorder.toLE PartialOrder.toPreorder instPartialOrderNNReal StrictMono Nat.instPreorder SuccDiffBounded	Summable NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring instSemiringNNReal instTopologicalSpace Distrib.toMul NonUnitalNonAssocSemiring.toDistrib instSub AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne SummationFilter.unconditional	—	ENNReal.coe_le_coe LT.lt.trans zero_lt_one Nat.instZeroLEOneClass ENNReal.instCharZero eq_top_mono ENNReal.tsum_schlomilch_le StrictMono.monotone ENNReal.sum_ne_top ENNReal.coe_ne_top ENNReal.coe_sub ENNReal.le_tsum_schlomilch

Real

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
not_summable_indicator_one_div_natCast 📖	mathematical	—	Summable Real instAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace pseudoMetricSpace Set.indicator instZero setOf ZMod AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing ZMod.commRing DivInvMonoid.toDiv instDivInvMonoid instOne instNatCast SummationFilter.unconditional	—	summable_nat_add_iff instIsTopologicalAddGroupReal Nat.cast_add Nat.cast_one Set.indicator_apply summable_indicator_mod_iff div_le_div₀ PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono instIsStrictOrderedRing MulPosReflectLE.toMulPosReflectLT MulPosStrictMono.toMulPosReflectLE IsStrictOrderedRing.toMulPosStrictMono le_of_lt Mathlib.Meta.Positivity.pos_of_isNat instIsOrderedRing instNontrivial Mathlib.Meta.NormNum.isNat_ofNat le_refl Nat.cast_pos' IsOrderedAddMonoid.toAddLeftMono instIsOrderedAddMonoid instZeroLEOneClass NeZero.charZero_one RCLike.charZero_rclike Right.add_pos_of_nonneg_of_pos covariant_swap_add_of_covariant_add Nat.instIsOrderedAddMonoid zero_le Nat.instCanonicallyOrderedAdd IsStrictOrderedRing.toIsOrderedRing Nat.instIsStrictOrderedRing Nat.instNontrivial Nat.mono_cast add_le_add_left not_summable_one_div_natCast
not_summable_natCast_inv 📖	mathematical	—	Summable Real instAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace pseudoMetricSpace instInv instNatCast SummationFilter.unconditional	—	summable_nat_pow_inv lt_irrefl pow_one
not_summable_one_div_natCast 📖	mathematical	—	Summable Real instAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace pseudoMetricSpace DivInvMonoid.toDiv instDivInvMonoid instOne instNatCast SummationFilter.unconditional	—	inv_eq_one_div not_summable_natCast_inv
summable_abs_int_rpow 📖	mathematical	Real instLT instOne	Summable instAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace pseudoMetricSpace instPow abs lattice instAddGroup instIntCast instNeg SummationFilter.unconditional	—	Summable.of_nat_of_neg instIsTopologicalAddGroupReal Int.cast_natCast abs_of_nonneg IsOrderedAddMonoid.toAddLeftMono instIsOrderedAddMonoid Nat.cast_nonneg instIsOrderedRing summable_nat_rpow neg_lt_neg_iff IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd IsRightCancelAdd.addRightStrictMono_of_addRightMono AddRightCancelSemigroup.toIsRightCancelAdd covariant_swap_add_of_covariant_add Int.cast_neg abs_neg
summable_nat_pow_inv 📖	mathematical	—	Summable Real instAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace pseudoMetricSpace instInv Monoid.toNatPow instMonoid instNatCast SummationFilter.unconditional	—	IsOrderedAddMonoid.toAddLeftMono instIsOrderedAddMonoid instZeroLEOneClass RCLike.charZero_rclike
summable_nat_rpow 📖	mathematical	—	Summable Real instAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace pseudoMetricSpace instPow instNatCast SummationFilter.unconditional instLT instNeg instOne	—	neg_surjective rpow_neg instIsOrderedRing IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd IsOrderedAddMonoid.toAddLeftMono instIsOrderedAddMonoid IsRightCancelAdd.addRightStrictMono_of_addRightMono AddRightCancelSemigroup.toIsRightCancelAdd covariant_swap_add_of_covariant_add
summable_nat_rpow_inv 📖	mathematical	—	Summable Real instAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace pseudoMetricSpace instInv instPow instNatCast SummationFilter.unconditional instLT instOne	—	le_or_gt Nat.instAtLeastTwoHAddOfNat summable_condensed_iff_of_nonneg inv_nonneg_of_nonneg PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono instIsStrictOrderedRing rpow_nonneg Nat.cast_nonneg' IsOrderedAddMonoid.toAddLeftMono instIsOrderedAddMonoid instZeroLEOneClass inv_anti₀ MulPosReflectLE.toMulPosReflectLT MulPosStrictMono.toMulPosReflectLE IsStrictOrderedRing.toMulPosStrictMono rpow_pos_of_pos Nat.cast_pos' NeZero.charZero_one RCLike.charZero_rclike rpow_le_rpow le_of_lt Nat.mono_cast Nat.cast_pow rpow_mul LT.lt.le zero_lt_two mul_comm rpow_natCast rpow_one division_def rpow_sub norm_eq_abs abs_of_pos rpow_lt_one_iff IsRightCancelAdd.addRightStrictMono_of_addRightMono AddRightCancelSemigroup.toIsRightCancelAdd covariant_swap_add_of_covariant_add Filter.Eventually.exists Filter.cofinite_neBot instInfiniteNat Filter.Eventually.and Filter.Tendsto.eventually Summable.tendsto_cofinite_zero instIsTopologicalAddGroupReal gt_mem_nhds instOrderTopologyReal zero_lt_one Filter.eventually_cofinite_ne inv_lt_one₀ Nat.cast_pos instIsOrderedRing instNontrivial pos_iff_ne_zero Nat.instCanonicallyOrderedAdd one_lt_rpow_iff_of_pos LT.lt.not_gt LT.lt.not_ge LE.le.trans zero_le_one
summable_one_div_int_add_rpow 📖	mathematical	—	Summable Real instAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace pseudoMetricSpace DivInvMonoid.toDiv instDivInvMonoid instOne instPow abs lattice instAddGroup instAdd instIntCast SummationFilter.unconditional instLT	—	instIsUniformAddGroupReal instCompleteSpace abs_neg neg_add Int.cast_neg neg_neg Int.cast_natCast
summable_one_div_int_pow 📖	mathematical	—	Summable Real instAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace pseudoMetricSpace DivInvMonoid.toDiv instDivInvMonoid instOne Monoid.toNatPow instMonoid instIntCast SummationFilter.unconditional	—	summable_one_div_nat_pow Summable.comp_injective instIsUniformAddGroupReal instCompleteSpace Nat.cast_injective Int.instCharZero Summable.of_nat_of_neg instIsTopologicalAddGroupReal Summable.congr Summable.mul_left IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal Int.cast_neg Int.cast_natCast neg_eq_neg_one_mul mul_pow mul_one_div div_div
summable_one_div_nat_add_rpow 📖	mathematical	—	Summable Real instAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace pseudoMetricSpace DivInvMonoid.toDiv instDivInvMonoid instOne instPow abs lattice instAddGroup instAdd instNatCast SummationFilter.unconditional instLT	—	summable_of_isBigO_nat instCompleteSpace Asymptotics.isBigO_of_div_tendsto_nhds Filter.mp_mem instIsStrictOrderedRing Filter.eventually_gt_atTop instNoTopOrderOfNoMaxOrder Nat.instNoMaxOrder 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.atom_pf Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.cast_zero Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_zero Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.neg_congr Mathlib.Tactic.Ring.neg_add Mathlib.Tactic.Ring.neg_mul 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.add_pf_add_gt Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Linarith.add_lt_of_le_of_neg Mathlib.Tactic.Linarith.sub_nonpos_of_le instIsOrderedRing Mathlib.Tactic.Linarith.sub_neg_of_lt lt_of_abs_lt Nat.lt_of_ceil_lt abs_neg ne_of_gt div_pos PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Mathlib.Meta.Positivity.pos_of_isNat instNontrivial Nat.cast_one rpow_pos_of_pos abs_pos_of_pos IsOrderedAddMonoid.toAddLeftMono instIsOrderedAddMonoid div_div mul_one_div one_div_div Filter.Tendsto.comp add_zero Filter.Tendsto.add IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal tendsto_const_nhds Filter.Tendsto.div_atTop instOrderTopologyReal Filter.tendsto_id Filter.Tendsto.congr' instNoMaxOrderOfNontrivial Mathlib.Tactic.FieldSimp.eq_eq_cancel_eq IsCancelMulZero.toIsLeftCancelMulZero instIsCancelMulZero Mathlib.Tactic.FieldSimp.eq_mul_of_eq_eq_eq_mul Mathlib.Tactic.FieldSimp.subst_add Mathlib.Tactic.FieldSimp.NF.one_eq_eval Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval_cons_neg LT.lt.ne' Mathlib.Tactic.Linarith.add_lt_of_neg_of_le one_mul Mathlib.Tactic.FieldSimp.eq_div_of_eq_one_of_subst Mathlib.Tactic.FieldSimp.NF.cons_eq_div_of_eq_div div_one Mathlib.Tactic.FieldSimp.NF.eval_cons Mathlib.Tactic.FieldSimp.zpow'_one Mathlib.Tactic.FieldSimp.NF.div_eq_eval Mathlib.Tactic.FieldSimp.subst_sub Mathlib.Tactic.FieldSimp.NF.atom_eq_eval Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons Mathlib.Tactic.FieldSimp.NF.div_eq_eval₃ Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₃ mul_one Mathlib.Tactic.FieldSimp.NF.div_eq_eval₁ Mathlib.Tactic.FieldSimp.NF.one_div_eq_eval Mathlib.Tactic.FieldSimp.NF.cons_ne_zero one_ne_zero NeZero.one GroupWithZero.toNontrivial add_add_sub_cancel Filter.Tendsto.atTop_add ContinuousAt.tendsto continuousAt_rpow_const NeZero.charZero_one RCLike.charZero_rclike one_rpow div_rpow LT.lt.le neg_lt_iff_pos_add IsRightCancelAdd.addRightStrictMono_of_addRightMono AddRightCancelSemigroup.toIsRightCancelAdd covariant_swap_add_of_covariant_add abs_of_pos tendsto_natCast_atTop_atTop instArchimedean Nat.abs_cast
summable_one_div_nat_pow 📖	mathematical	—	Summable Real instAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace pseudoMetricSpace DivInvMonoid.toDiv instDivInvMonoid instOne Monoid.toNatPow instMonoid instNatCast SummationFilter.unconditional	—	one_div
summable_one_div_nat_rpow 📖	mathematical	—	Summable Real instAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace pseudoMetricSpace DivInvMonoid.toDiv instDivInvMonoid instOne instPow instNatCast SummationFilter.unconditional instLT	—	one_div
tendsto_sum_range_one_div_nat_succ_atTop 📖	mathematical	—	Filter.Tendsto Real Finset.sum instAddCommMonoid Finset.range DivInvMonoid.toDiv instDivInvMonoid instOne instAdd instNatCast Filter.atTop Nat.instPreorder instPreorder	—	not_summable_iff_tendsto_nat_atTop_of_nonneg le_of_lt div_pos PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono instIsStrictOrderedRing Mathlib.Meta.Positivity.pos_of_isNat instIsOrderedRing instNontrivial Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one Right.add_pos_of_nonneg_of_pos covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono instIsOrderedAddMonoid Nat.cast_nonneg' instZeroLEOneClass summable_nat_add_iff instIsTopologicalAddGroupReal not_summable_one_div_natCast

(root)

Definitions

Name	Category	Theorems
SuccDiffBounded 📖	MathDef	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
sum_Ioc_inv_sq_le_sub 📖	mathematical	—	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Finset.sum NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Field.toCommRing Finset.Ioc Nat.instPreorder Nat.instLocallyFiniteOrder InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid DivisionCommMonoid.toDivisionMonoid CommGroupWithZero.toDivisionCommMonoid Semifield.toCommGroupWithZero Field.toSemifield Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne DivisionRing.toRing Field.toDivisionRing SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup	—	Nat.le_induction Finset.sum_congr Finset.Ioc_self sub_self Finset.sum_Ioc_succ_top le_imp_le_of_le_of_le add_le_add_left covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono IsOrderedRing.toIsOrderedAddMonoid IsStrictOrderedRing.toIsOrderedRing le_refl Nat.cast_add Nat.cast_one IsSimpleRing.instNontrivial DivisionRing.isSimpleRing LT.lt.trans_le Ne.bot_lt Mathlib.Tactic.FieldSimp.le_eq_cancel_le PosMulStrictMono.toPosMulMono IsStrictOrderedRing.toPosMulStrictMono PosMulStrictMono.toPosMulReflectLE Mathlib.Tactic.FieldSimp.eq_mul_of_eq_eq_eq_mul Mathlib.Tactic.FieldSimp.subst_add Mathlib.Tactic.FieldSimp.subst_sub Mathlib.Tactic.FieldSimp.NF.inv_eq_eval Mathlib.Tactic.FieldSimp.NF.atom_eq_eval Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval_cons_neg ne_of_gt Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval one_mul Mathlib.Tactic.FieldSimp.eq_div_of_eq_one_of_subst Mathlib.Tactic.FieldSimp.NF.cons_eq_div_of_eq_div div_one Mathlib.Tactic.FieldSimp.NF.eval_cons Mathlib.Tactic.FieldSimp.zpow'_one Nat.cast_pos' IsStrictOrderedRing.toZeroLEOneClass NeZero.charZero_one IsStrictOrderedRing.toCharZero lt_of_le_of_ne' zero_le Nat.instCanonicallyOrderedAdd Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₃ mul_one add_pos' Mathlib.Meta.Positivity.pos_of_isNat Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons Mathlib.Tactic.FieldSimp.zpow'_ofNat Mathlib.Tactic.FieldSimp.NF.pow_eq_eval Mathlib.Tactic.FieldSimp.NF.one_eq_eval Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₂ LT.lt.ne' Mathlib.Tactic.FieldSimp.NF.cons_pos PosMulReflectLE.toPosMulReflectLT zero_lt_one NeZero.one GroupWithZero.toNontrivial 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.cast_zero Nat.cast_zero Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_add Mathlib.Tactic.Ring.neg_mul 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.add_pf_zero_add Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.mul_pp_pf_overlap Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.isNat_add Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.add_pf_add_overlap Mathlib.Tactic.Ring.add_overlap_pf Mathlib.Tactic.Ring.pow_congr Mathlib.Tactic.Ring.pow_add Mathlib.Tactic.Ring.pow_nat Mathlib.Tactic.Ring.coeff_one Mathlib.Tactic.Ring.pow_one_cast Mathlib.Tactic.Ring.pow_bit0 Mathlib.Tactic.Ring.pow_one Mathlib.Tactic.Ring.pow_zero Mathlib.Tactic.Ring.mul_one Mathlib.Meta.NormNum.isInt_add Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Tactic.Linarith.add_lt_of_le_of_neg Mathlib.Tactic.Linarith.sub_nonpos_of_le Mathlib.Tactic.Linarith.natCast_nonneg Mathlib.Tactic.Linarith.sub_neg_of_lt
sum_Ioo_inv_sq_le 📖	mathematical	—	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Finset.sum NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Field.toCommRing Finset.Ioo Nat.instPreorder Nat.instLocallyFiniteOrder InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid DivisionCommMonoid.toDivisionMonoid CommGroupWithZero.toDivisionCommMonoid Semifield.toCommGroupWithZero Field.toSemifield Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne DivisionRing.toRing Field.toDivisionRing DivInvMonoid.toDiv DivisionRing.toDivInvMonoid instOfNatAtLeastTwo Nat.instAtLeastTwoHAddOfNat Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib AddMonoidWithOne.toOne	—	Nat.instAtLeastTwoHAddOfNat Finset.sum_le_sum_of_subset_of_nonneg IsOrderedAddMonoid.toAddLeftMono IsOrderedRing.toIsOrderedAddMonoid IsStrictOrderedRing.toIsOrderedRing LT.lt.le inv_nonneg_of_nonneg PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Even.pow_nonneg AddGroup.existsAddOfLE even_two_mul Finset.Icc_add_one_left_eq_Ioc Nat.instNoMaxOrder Finset.Ico_add_one_right_eq_Icc Finset.sum_eq_sum_Ico_succ_bot LT.lt.trans_le le_max_left Nat.cast_one Finset.sum_congr le_refl add_le_add covariant_swap_add_of_covariant_add le_rfl LE.le.trans sum_Ioc_inv_sq_le_sub Nat.cast_succ IsRightCancelAdd.addRightReflectLE_of_addRightReflectLT AddRightCancelSemigroup.toIsRightCancelAdd contravariant_swap_add_of_contravariant_add contravariant_lt_of_covariant_le add_le_add_left div_le_div₀ MulPosReflectLE.toMulPosReflectLT MulPosStrictMono.toMulPosReflectLE IsStrictOrderedRing.toMulPosStrictMono le_of_lt Mathlib.Meta.Positivity.pos_of_isNat IsSimpleRing.instNontrivial DivisionRing.isSimpleRing Mathlib.Meta.NormNum.isNat_ofNat Right.add_pos_of_nonneg_of_pos Nat.cast_nonneg' IsStrictOrderedRing.toZeroLEOneClass pow_one pow_right_mono₀ IsOrderedRing.toPosMulMono one_le_two Nat.instZeroLEOneClass Nat.instIsOrderedAddMonoid Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.div_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.div_pf Mathlib.Tactic.Ring.atom_pf' 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.zero_mul Mathlib.Tactic.Ring.add_pf_add_overlap Mathlib.Tactic.Ring.add_overlap_pf Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.isNat_add Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Meta.NormNum.instAtLeastTwo Mathlib.Tactic.Ring.mul_one
summable_condensed_iff_of_eventually_nonneg 📖	mathematical	Filter.EventuallyLE Real Real.instLE Filter.atTop Nat.instPreorder Pi.instZero Real.instZero Filter.Eventually	Summable Real.instAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Real.instMul Monoid.toNatPow Real.instMonoid instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat Nat.instMonoid SummationFilter.unconditional	—	Nat.instAtLeastTwoHAddOfNat Filter.eventually_atTop instIsDirectedOrder IsStrictOrderedRing.toIsOrderedRing Nat.instIsStrictOrderedRing instArchimedeanNat Filter.EventuallyLE.eq_1 summable_congr_atTop instIsTopologicalAddGroupReal tendsto_pow_atTop_atTop_of_one_lt StarOrderedRing.toExistsAddOfLE Nat.instStarOrderedRing IsOrderedAddMonoid.toAddLeftMono Nat.instIsOrderedAddMonoid Nat.instZeroLEOneClass Nat.instCharZero Filter.mp_mem Filter.Tendsto.eventually_ge_atTop Filter.univ_mem' max_eq_left Filter.eventually_ge_atTop summable_condensed_iff_of_nonneg Mathlib.Tactic.Bound.le_max_of_le_left_or_le_right IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT AddLeftCancelSemigroup.toIsLeftCancelAdd contravariant_lt_of_covariant_le Nat.instCanonicallyOrderedAdd antitoneOn_nat_Ici_of_succ_le le_of_not_gt Mathlib.Tactic.Linarith.lt_irrefl Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.neg_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat 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.sub_congr Mathlib.Tactic.Ring.cast_zero Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_mul Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Linarith.add_lt_of_neg_of_le Int.instIsStrictOrderedRing neg_neg_of_pos Int.instIsOrderedAddMonoid Mathlib.Tactic.Linarith.zero_lt_one Mathlib.Tactic.Linarith.sub_nonpos_of_le Mathlib.Tactic.Linarith.natCast_nonneg Nat.cast_add max_le le_max_right
summable_condensed_iff_of_nonneg 📖	mathematical	Real Real.instLE Real.instZero	Summable Real.instAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Real.instMul Monoid.toNatPow Real.instMonoid instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat Nat.instMonoid SummationFilter.unconditional	—	pow_succ mul_two add_tsub_cancel_right Nat.instOrderedSub IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT AddLeftCancelSemigroup.toIsLeftCancelAdd contravariant_lt_of_covariant_le IsOrderedAddMonoid.toAddLeftMono Nat.instIsOrderedAddMonoid two_mul Nat.instAtLeastTwoHAddOfNat Nat.cast_add Nat.cast_pow add_sub_cancel_right summable_schlomilch_iff_of_nonneg pow_pos LinearOrderedCommMonoidWithZero.toPosMulStrictMono Nat.instZeroLEOneClass zero_lt_two pow_right_strictMono₀ one_lt_two IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono two_ne_zero
summable_pow_div_add 📖	mathematical	—	Summable Real Real.instAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Norm.norm NormedField.toNorm DenselyNormedField.toNormedField RCLike.toDenselyNormedField DivInvMonoid.toDiv DivisionRing.toDivInvMonoid NormedDivisionRing.toDivisionRing NormedField.toNormedDivisionRing Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne NormedRing.toRing NormedCommRing.toNormedRing SummationFilter.unconditional	—	norm_div Summable.const_div IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal norm_pow NormedDivisionRing.to_normOneClass NormedDivisionRing.toNormMulClass one_div Nat.cast_add norm_inv norm_natCast RCLike.instNormSMulClassInt summable_nat_add_iff instIsTopologicalAddGroupReal
summable_schlomilch_iff_of_nonneg 📖	mathematical	Real Real.instLE Real.instZero StrictMono Nat.instPreorder SuccDiffBounded	Summable Real.instAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Real.instMul Real.instSub Real.instNatCast SummationFilter.unconditional	—	CanLift.prf Pi.canLift NNReal.canLift Nat.cast_le NNReal.addLeftMono LinearOrderedCommMonoidWithZero.toZeroLeOneClass IsStrictOrderedRing.toCharZero NNReal.instIsStrictOrderedRing LT.lt.le NNReal.coe_sub NNReal.coe_natCast NNReal.instIsOrderedRing NNReal.instCanonicallyOrderedAdd NNReal.instOrderedSub IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT AddLeftCancelSemigroup.toIsLeftCancelAdd NNReal.addLeftReflectLT NNReal.summable_schlomilch_iff

---

← Back to Index