OfDigits

📁 Source: Mathlib/Analysis/Real/OfDigits.lean

Statistics

Metric	Count
Definitions digits, ofDigits, ofDigitsTerm	3
Theorems abs_ofDigits_sub_ofDigits_le, continuous_ofDigits, hasSum_ofDigitsTerm_digits, le_sum_ofDigitsTerm_digits, ofDigitsTerm_le, ofDigitsTerm_nonneg, ofDigits_SurjOn, ofDigits_const_last_eq_one, ofDigits_const_last_eq_one', ofDigits_digits, ofDigits_digits_sum_eq, ofDigits_eq_sum_add_ofDigits, ofDigits_le_one, ofDigits_nonneg, sum_ofDigitsTerm_digits_le, summable_ofDigitsTerm	16
Total	19

Real

Definitions

Name	Category	Theorems
digits 📖	CompOp	5 math math: sum_ofDigitsTerm_digits_le, hasSum_ofDigitsTerm_digits, le_sum_ofDigitsTerm_digits, ofDigits_digits, ofDigits_digits_sum_eq
ofDigits 📖	CompOp	13 math math: ofDigits_const_last_eq_one, ofDigits_zero_two_sequence_mem_cantorSet, ofDigits_cantorToTernary, ofDigits_bool_to_fin_three_mem_cantorSet, ofDigits_eq_sum_add_ofDigits, ofDigits_SurjOn, cantorSet_eq_zero_two_ofDigits, ofDigits_nonneg, ofDigits_digits, continuous_ofDigits, abs_ofDigits_sub_ofDigits_le, ofDigits_const_last_eq_one', ofDigits_le_one
ofDigitsTerm 📖	CompOp	12 math math: summable_ofDigitsTerm, sum_ofDigitsTerm_digits_le, le_ofDigits_cantorToTernary_sum, ofDigitsTerm_le, hasSum_ofDigitsTerm_digits, ofDigits_eq_sum_add_ofDigits, le_sum_ofDigitsTerm_digits, ofDigitsTerm_nonneg, ofDigits_cantorToTernary_sum_le, cantorSequence_eq_self_sub_sum_cantorToTernary, cantorSequence_get_succ, ofDigits_digits_sum_eq

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
abs_ofDigits_sub_ofDigits_le 📖	mathematical	—	Real instLE abs lattice instAddGroup instSub ofDigits instInv Monoid.toNatPow instMonoid instNatCast	—	ofDigits_eq_sum_add_ofDigits Finset.sum_congr Finset.mem_range add_sub_add_left_eq_sub mul_sub abs_mul instIsOrderedRing abs_of_nonneg IsOrderedAddMonoid.toAddLeftMono instIsOrderedAddMonoid inv_nonneg_of_nonneg PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono instIsStrictOrderedRing pow_nonneg IsOrderedRing.toZeroLEOneClass IsOrderedRing.toPosMulMono Nat.cast_nonneg' instZeroLEOneClass mul_le_of_le_one_right sub_zero abs_sub_le_of_le_of_le ofDigits_nonneg ofDigits_le_one
continuous_ofDigits 📖	mathematical	—	Continuous Real Pi.topologicalSpace instTopologicalSpaceFin UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace pseudoMetricSpace ofDigits	—	continuous_of_discreteTopology Finite.instDiscreteTopology instT1SpaceForall T5Space.toT1Space OrderTopology.t5Space OrderTopology.of_linearLocallyFinite instDiscreteTopologyFin Finite.of_subsingleton Finite.of_fintype continuous_tsum instCompleteSpace Continuous.comp' Continuous.fun_mul IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal Continuous.fst continuous_id' Continuous.snd Continuous.prodMk continuous_const instDiscreteTopologyNat continuous_apply summable_geometric_of_lt_one le_of_lt inv_pos_of_pos PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono instIsStrictOrderedRing lt_trans Mathlib.Meta.Positivity.pos_of_isNat instIsOrderedRing instNontrivial Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one Int.cast_one Int.cast_natCast Rat.cast_one Rat.cast_natCast inv_lt_one_of_one_lt₀ instZeroLEOneClass abs_of_nonneg IsOrderedAddMonoid.toAddLeftMono instIsOrderedAddMonoid ofDigitsTerm_nonneg inv_pow LE.le.trans ofDigitsTerm_le mul_le_mul_of_nonneg_right IsOrderedRing.toMulPosMono 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.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.atom_pf Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Tactic.Ring.neg_mul Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.cast_zero Nat.cast_zero Mathlib.Tactic.Linarith.add_neg neg_neg_of_pos Mathlib.Tactic.Linarith.zero_lt_one Mathlib.Tactic.Linarith.sub_neg_of_lt pow_pos IsStrictOrderedRing.toZeroLEOneClass
hasSum_ofDigitsTerm_digits 📖	mathematical	Real Set Set.instMembership Set.Ico instPreorder instZero instOne	HasSum instAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace pseudoMetricSpace ofDigitsTerm digits SummationFilter.unconditional	—	hasSum_iff_tendsto_nat_of_summable_norm Summable.abs instIsOrderedAddMonoid instIsUniformAddGroupReal instCompleteSpace summable_ofDigitsTerm tendsto_of_tendsto_of_tendsto_of_le_of_le instOrderTopologyReal sub_zero Filter.Tendsto.sub IsTopologicalAddGroup.to_continuousSub instIsTopologicalAddGroupReal tendsto_const_nhds tendsto_pow_atTop_nhds_zero_of_abs_lt_one abs_of_nonneg IsOrderedAddMonoid.toAddLeftMono PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono instIsStrictOrderedRing instIsOrderedRing instZeroLEOneClass IsStrictOrderedRing.toCharZero le_sum_ofDigitsTerm_digits sum_ofDigitsTerm_digits_le
le_sum_ofDigitsTerm_digits 📖	mathematical	Real Set Set.instMembership Set.Ico instPreorder instZero instOne	instLE instSub Monoid.toNatPow instMonoid instInv instNatCast Finset.sum instAddCommMonoid Finset.range ofDigitsTerm digits	—	NeZero.pos Nat.instCanonicallyOrderedAdd instIsStrictOrderedRing ofDigits_digits_sum_eq Nat.lt_floor_add_one mul_le_mul_iff_right₀ IsOrderedRing.toPosMulMono instIsOrderedRing PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono pow_pos IsStrictOrderedRing.toZeroLEOneClass Nat.cast_pos' IsOrderedAddMonoid.toAddLeftMono instIsOrderedAddMonoid instZeroLEOneClass NeZero.one instNontrivial mul_sub inv_pow mul_inv_cancel₀ ne_of_gt 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.mul_congr Mathlib.Tactic.Ring.pow_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.pow_add Mathlib.Tactic.Ring.single_pow Mathlib.Tactic.Ring.mul_pow Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.one_pow Mathlib.Tactic.Ring.pow_zero Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one 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_mul Mathlib.Tactic.Ring.neg_zero Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Tactic.Ring.cast_zero Nat.cast_zero Mathlib.Tactic.Linarith.add_neg Mathlib.Tactic.Linarith.sub_neg_of_lt
ofDigitsTerm_le 📖	mathematical	—	Real instLE ofDigitsTerm instMul instSub instNatCast instOne instInv Monoid.toNatPow instMonoid	—	mul_le_mul_of_nonneg_right IsOrderedRing.toMulPosMono instIsOrderedRing Nat.cast_add Nat.cast_one add_sub_cancel_right IsOrderedAddMonoid.toAddLeftMono instIsOrderedAddMonoid instZeroLEOneClass IsStrictOrderedRing.toCharZero instIsStrictOrderedRing le_of_lt inv_pos_of_pos PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono pow_pos IsStrictOrderedRing.toZeroLEOneClass Nat.cast_pos' NeZero.one instNontrivial Right.add_pos_of_nonneg_of_pos covariant_swap_add_of_covariant_add Nat.instIsOrderedAddMonoid zero_le Nat.instCanonicallyOrderedAdd Mathlib.Meta.Positivity.pos_of_isNat IsStrictOrderedRing.toIsOrderedRing Nat.instIsStrictOrderedRing Nat.instNontrivial Mathlib.Meta.NormNum.isNat_ofNat
ofDigitsTerm_nonneg 📖	mathematical	—	Real instLE instZero ofDigitsTerm	—	mul_nonneg IsOrderedRing.toPosMulMono instIsOrderedRing Nat.cast_nonneg' IsOrderedAddMonoid.toAddLeftMono instIsOrderedAddMonoid instZeroLEOneClass inv_nonneg_of_nonneg PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono instIsStrictOrderedRing pow_nonneg IsOrderedRing.toZeroLEOneClass
ofDigits_SurjOn 📖	mathematical	—	Set.SurjOn Real ofDigits Set.univ Set.Icc instPreorder instZero instOne	—	ofDigits_digits Set.image_univ ofDigits_const_last_eq_one'
ofDigits_const_last_eq_one 📖	mathematical	—	ofDigits Real instOne	—	Nat.cast_add_one abs_of_nonneg IsOrderedAddMonoid.toAddLeftMono instIsOrderedAddMonoid Nat.cast_nonneg instIsOrderedRing Nat.cast_add Nat.cast_one IsRightCancelAdd.addRightStrictMono_of_addRightMono AddRightCancelSemigroup.toIsRightCancelAdd covariant_swap_add_of_covariant_add contravariant_swap_add_of_contravariant_add contravariant_lt_of_covariant_le instNontrivial NeZero.pos Nat.instCanonicallyOrderedAdd Summable.tsum_mul_left IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace SummationFilter.instNeBotUnconditional summable_nat_add_iff instIsTopologicalAddGroupReal summable_geometric_of_lt_one le_of_lt inv_pos_of_pos PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono instIsStrictOrderedRing Nat.cast_pos' instZeroLEOneClass NeZero.one Right.add_pos_of_nonneg_of_pos Nat.instIsOrderedAddMonoid zero_le Mathlib.Meta.Positivity.pos_of_isNat IsStrictOrderedRing.toIsOrderedRing Nat.instIsStrictOrderedRing Nat.instNontrivial Mathlib.Meta.NormNum.isNat_ofNat geom_series_succ instHasSummableGeomSeries norm_inv tsum_geometric_of_lt_one Nat.cast_zero IsStrictOrderedRing.toCharZero Mathlib.Tactic.FieldSimp.eq_eq_cancel_eq IsCancelMulZero.toIsLeftCancelMulZero instIsCancelMulZero Mathlib.Tactic.FieldSimp.eq_mul_of_eq_eq_eq_mul Mathlib.Tactic.FieldSimp.NF.mul_eq_eval Mathlib.Tactic.FieldSimp.NF.atom_eq_eval Mathlib.Tactic.FieldSimp.subst_sub Mathlib.Tactic.FieldSimp.NF.inv_eq_eval Mathlib.Tactic.FieldSimp.NF.one_eq_eval Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval_cons_neg ne_of_gt add_pos' lt_of_le_of_ne' Nat.cast_nonneg' 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.subst_add Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₃ mul_one add_sub_cancel_right Mathlib.Tactic.FieldSimp.NF.cons_ne_zero one_ne_zero GroupWithZero.toNontrivial Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.add_pf_add_zero 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 Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Ring.neg_mul Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Tactic.Ring.add_pf_zero_add 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_zero Mathlib.Tactic.Ring.zero_mul
ofDigits_const_last_eq_one' 📖	mathematical	—	ofDigits Real instOne	—	Function.hfunext ofDigits_const_last_eq_one
ofDigits_digits 📖	mathematical	Real Set Set.instMembership Set.Ico instPreorder instZero instOne	ofDigits digits	—	Summable.hasSum_iff TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace SummationFilter.instNeBotUnconditional summable_ofDigitsTerm hasSum_ofDigitsTerm_digits
ofDigits_digits_sum_eq 📖	mathematical	Real Set Set.instMembership Set.Ico instPreorder instZero instOne	instMul Monoid.toNatPow instMonoid instNatCast Finset.sum instAddCommMonoid Finset.range ofDigitsTerm digits Nat.floor semiring partialOrder FloorRing.toFloorSemiring instRing linearOrder instIsStrictOrderedRing instFloorRing	—	instIsStrictOrderedRing pow_zero MulZeroClass.mul_zero one_mul Nat.floor_eq_zero CharP.cast_eq_zero CharP.ofCharZero IsStrictOrderedRing.toCharZero Finset.sum_range_succ mul_add Distrib.leftDistribClass pow_succ' mul_assoc ofDigitsTerm.eq_1 digits.eq_1 mul_left_comm mul_inv_cancel₀ ne_of_gt pow_pos IsStrictOrderedRing.toPosMulStrictMono IsStrictOrderedRing.toZeroLEOneClass Nat.cast_pos' IsOrderedAddMonoid.toAddLeftMono instIsOrderedAddMonoid instZeroLEOneClass NeZero.one instNontrivial lt_of_le_of_ne' zero_le Nat.instCanonicallyOrderedAdd mul_one mul_comm Nat.cast_mul_floor_div_cancel
ofDigits_eq_sum_add_ofDigits 📖	mathematical	—	ofDigits Real instAdd Finset.sum instAddCommMonoid Finset.range ofDigitsTerm instMul instInv Monoid.toNatPow instMonoid instNatCast	—	Summable.sum_add_tsum_nat_add instIsTopologicalAddGroupReal TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace summable_ofDigitsTerm Summable.tsum_mul_left IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal SummationFilter.instNeBotUnconditional Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.inv_congr Mathlib.Tactic.Ring.pow_congr Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.pow_add Mathlib.Tactic.Ring.pow_one_cast Mathlib.Tactic.Ring.single_pow Mathlib.Tactic.Ring.mul_pow Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.one_pow Mathlib.Tactic.Ring.pow_zero Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.zero_mul 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 IsStrictOrderedRing.toCharZero instIsStrictOrderedRing Mathlib.Meta.NormNum.IsNat.to_isNNRat Mathlib.Meta.NormNum.IsNat.of_raw
ofDigits_le_one 📖	mathematical	—	Real instLE ofDigits instOne	—	LE.le.eq_or_lt CharP.cast_eq_zero CharP.ofCharZero IsStrictOrderedRing.toCharZero instIsStrictOrderedRing Nat.cast_one one_pow inv_one mul_one tsum_zero instZeroLEOneClass pow_succ' mul_inv tsum_mul_left IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace tsum_geometric_of_lt_one le_of_lt inv_pos_of_pos PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono lt_trans Mathlib.Meta.Positivity.pos_of_isNat instIsOrderedRing instNontrivial Mathlib.Meta.NormNum.isNat_ofNat Int.cast_one Int.cast_natCast Rat.cast_one Rat.cast_natCast IsOrderedAddMonoid.toAddLeftMono instIsOrderedAddMonoid sub_pos IsRightCancelAdd.addRightStrictMono_of_addRightMono AddRightCancelSemigroup.toIsRightCancelAdd covariant_swap_add_of_covariant_add Mathlib.Tactic.FieldSimp.eq_eq_cancel_eq IsCancelMulZero.toIsLeftCancelMulZero instIsCancelMulZero Mathlib.Tactic.FieldSimp.eq_mul_of_eq_eq_eq_mul Mathlib.Tactic.FieldSimp.NF.one_eq_eval one_mul Mathlib.Tactic.FieldSimp.eq_div_of_eq_one_of_subst div_one Mathlib.Tactic.FieldSimp.NF.mul_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.cons_eq_div_of_eq_div Mathlib.Tactic.FieldSimp.NF.eval_cons Mathlib.Tactic.FieldSimp.zpow'_one Mathlib.Tactic.FieldSimp.NF.inv_eq_eval Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₁ Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval_cons_neg ne_of_gt Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₃ 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 one_ne_zero NeZero.one GroupWithZero.toNontrivial Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.cast_pos Summable.tsum_mono HasSolidNorm.orderClosedTopology instHasSolidNormReal SummationFilter.instNeBotUnconditional summable_ofDigitsTerm Summable.mul_left summable_geometric_of_lt_one ofDigitsTerm_le
ofDigits_nonneg 📖	mathematical	—	Real instLE instZero ofDigits	—	tsum_nonneg instIsOrderedAddMonoid HasSolidNorm.orderClosedTopology instHasSolidNormReal ofDigitsTerm_nonneg
sum_ofDigitsTerm_digits_le 📖	mathematical	Real Set Set.instMembership Set.Ico instPreorder instZero instOne	instLE Finset.sum instAddCommMonoid Finset.range ofDigitsTerm digits	—	instIsStrictOrderedRing ofDigits_digits_sum_eq Nat.floor_le mul_nonneg IsOrderedRing.toPosMulMono instIsOrderedRing pow_nonneg IsOrderedRing.toZeroLEOneClass Nat.cast_nonneg' IsOrderedAddMonoid.toAddLeftMono instIsOrderedAddMonoid instZeroLEOneClass mul_le_mul_iff_of_pos_left PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono pow_pos IsStrictOrderedRing.toZeroLEOneClass Nat.cast_pos' NeZero.one instNontrivial lt_of_le_of_ne' zero_le Nat.instCanonicallyOrderedAdd
summable_ofDigitsTerm 📖	mathematical	—	Summable Real instAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace pseudoMetricSpace ofDigitsTerm SummationFilter.unconditional	—	Summable.of_nonneg_of_le ofDigitsTerm_nonneg ofDigitsTerm_le LE.le.eq_or_lt Nat.cast_one sub_self one_pow inv_one mul_one pow_succ' mul_inv Summable.mul_left IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal summable_geometric_of_lt_one le_of_lt inv_pos_of_pos PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono instIsStrictOrderedRing Nat.cast_pos' IsOrderedAddMonoid.toAddLeftMono instIsOrderedAddMonoid instZeroLEOneClass NeZero.one instNontrivial lt_trans Mathlib.Meta.Positivity.pos_of_isNat IsStrictOrderedRing.toIsOrderedRing Nat.instIsStrictOrderedRing Nat.instNontrivial Mathlib.Meta.NormNum.isNat_ofNat IsStrictOrderedRing.toCharZero

---

← Back to Index