Lemmas

📁 Source: Mathlib/Data/Nat/Digits/Lemmas.lean

Statistics

Metric	Count
Definitions consFixedLengthDigits, fixedLengthDigits, digitsAppend	3
Theorems card_fixedLengthDigits, consFixedLengthDigits_head, cons_mem_fixedLengthDigits_succ, fixedLengthDigits_one, fixedLengthDigits_succ_eq_disjiUnion, fixedLengthDigits_zero, mem_fixedLengthDigits_iff, ne_empty_of_mem_consFixedLengthDigits, pairwiseDisjoint_consFixedLengthDigits, sum_fixedLengthDigits_sum, base_pow_length_digits_le, base_pow_length_digits_le', bijOn_digitsAppend, bijOn_digitsAppend', bijOn_ofDigits, bijOn_ofDigits', digits_append_digits, digits_append_zeroes_append_digits, digits_len, digits_len_le_digits_len_succ, digits_length_le_iff, digits_two_eq_bits, dvd_ofDigits_sub_ofDigits, getD_digits, getLast_digit_ne_zero, head!_digits, injOn_ofDigits, le_digits_len_le, length_digitsAppend, lt_digits_length_iff, lt_of_mem_digitsAppend, mapsTo_digitsAppend, mapsTo_ofDigits, modEq_digits_sum, ofDigits_eq_sum_mapIdx, ofDigits_eq_sum_mapIdx_aux, ofDigits_mod, ofDigits_modEq, ofDigits_modEq', ofDigits_mod_eq_head!, ofDigits_neg_one, ofDigits_zmod, ofDigits_zmodeq, ofDigits_zmodeq', pow_length_le_mul_ofDigits, setInvOn_digitsAppend_ofDigits, sub_one_mul_sum_div_pow_eq_sub_sum_digits, sub_one_mul_sum_log_div_pow_eq_sub_sum_digits, sum_digits_ofDigits_eq_sum, sum_sum_digits_eq, zmodeq_ofDigits_digits	51
Total	54

List

Definitions

Name	Category	Theorems
consFixedLengthDigits 📖	CompOp	2 math math: fixedLengthDigits_succ_eq_disjiUnion, pairwiseDisjoint_consFixedLengthDigits
fixedLengthDigits 📖	CompOp	8 math math: Nat.bijOn_digitsAppend', card_fixedLengthDigits, fixedLengthDigits_succ_eq_disjiUnion, fixedLengthDigits_one, Nat.bijOn_ofDigits', fixedLengthDigits_zero, sum_fixedLengthDigits_sum, mem_fixedLengthDigits_iff

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
card_fixedLengthDigits 📖	mathematical	—	Finset.card fixedLengthDigits Monoid.toNatPow Nat.instMonoid	—	Set.BijOn.finsetCard_eq Nat.bijOn_ofDigits' Finset.card_range
consFixedLengthDigits_head 📖	mathematical	Finset Finset.instMembership consFixedLengthDigits	ne_empty_of_mem_consFixedLengthDigits	—	ne_empty_of_mem_consFixedLengthDigits Finset.mem_image
cons_mem_fixedLengthDigits_succ 📖	—	Finset Finset.instMembership fixedLengthDigits	—	—	mem_fixedLengthDigits_iff
fixedLengthDigits_one 📖	mathematical	—	fixedLengthDigits Finset.image Finset.range	—	Finset.ext mem_fixedLengthDigits_iff
fixedLengthDigits_succ_eq_disjiUnion 📖	mathematical	—	fixedLengthDigits Finset.disjiUnion Finset.range consFixedLengthDigits pairwiseDisjoint_consFixedLengthDigits	—	Finset.ext pairwiseDisjoint_consFixedLengthDigits Finset.disjiUnion_eq_biUnion mem_fixedLengthDigits_iff IsRightCancelAdd.addRightStrictMono_of_addRightMono AddRightCancelSemigroup.toIsRightCancelAdd covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono Nat.instIsOrderedAddMonoid contravariant_swap_add_of_contravariant_add contravariant_lt_of_covariant_le Nat.instNoMaxOrder Nat.instCanonicallyOrderedAdd cons_mem_fixedLengthDigits_succ
fixedLengthDigits_zero 📖	mathematical	—	fixedLengthDigits Finset Finset.instSingleton	—	Finset.ext Nat.mapsTo_ofDigits
mem_fixedLengthDigits_iff 📖	mathematical	—	Finset Finset.instMembership fixedLengthDigits	—	Nat.mapsTo_ofDigits
ne_empty_of_mem_consFixedLengthDigits 📖	—	Finset Finset.instMembership consFixedLengthDigits	—	—	Finset.mem_image
pairwiseDisjoint_consFixedLengthDigits 📖	mathematical	—	Set.PairwiseDisjoint Finset Finset.partialOrder Finset.instOrderBot SetLike.coe Finset.instSetLike Finset.range consFixedLengthDigits	—	Finset.pairwiseDisjoint_iff ne_empty_of_mem_consFixedLengthDigits Finset.mem_inter consFixedLengthDigits_head
sum_fixedLengthDigits_sum 📖	mathematical	—	Finset.sum Nat.instAddCommMonoid fixedLengthDigits MulZeroClass.toZero Nat.instMulZeroClass Monoid.toNatPow Nat.instMonoid Nat.choose	—	Finset.sum_congr fixedLengthDigits_zero Finset.sum_singleton zero_tsub Nat.instCanonicallyOrderedAdd Nat.instOrderedSub pow_zero mul_one MulZeroClass.zero_mul fixedLengthDigits.congr_simp zero_add fixedLengthDigits_one Finset.sum_image Finset.coe_range add_zero Finset.sum_range_id tsub_self Nat.choose_two_right one_mul pairwiseDisjoint_consFixedLengthDigits fixedLengthDigits_succ_eq_disjiUnion Finset.sum_disjiUnion Finset.sum_comm Finset.sum_add_distrib Finset.sum_const Finset.sum_nsmul nsmul_eq_mul Finset.card_range add_tsub_cancel_right IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT AddLeftCancelSemigroup.toIsLeftCancelAdd contravariant_lt_of_covariant_le IsOrderedAddMonoid.toAddLeftMono Nat.instIsOrderedAddMonoid card_fixedLengthDigits Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.pow_congr 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.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

Nat

Definitions

Name	Category	Theorems
digitsAppend 📖	CompOp	5 math math: bijOn_digitsAppend', length_digitsAppend, mapsTo_digitsAppend, setInvOn_digitsAppend_ofDigits, bijOn_digitsAppend

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
base_pow_length_digits_le 📖	mathematical	—	Monoid.toNatPow instMonoid digits	—	instCanonicallyOrderedAdd zero_add base_pow_length_digits_le'
base_pow_length_digits_le' 📖	mathematical	—	Monoid.toNatPow instMonoid digits	—	digits_ne_nil_iff_ne_zero ofDigits_digits pow_length_le_mul_ofDigits getLast_digit_ne_zero
bijOn_digitsAppend 📖	mathematical	—	Set.BijOn digitsAppend setOf Monoid.toNatPow instMonoid	—	Set.BijOn.symm Set.InvOn.symm setInvOn_digitsAppend_ofDigits bijOn_ofDigits
bijOn_digitsAppend' 📖	mathematical	—	Set.BijOn digitsAppend SetLike.coe Finset Finset.instSetLike Finset.range Monoid.toNatPow instMonoid List.fixedLengthDigits	—	mapsTo_ofDigits Set.coe_toFinset Set.ext Finset.coe_range bijOn_digitsAppend
bijOn_ofDigits 📖	mathematical	—	Set.BijOn ofDigits instSemiring setOf Monoid.toNatPow instMonoid	—	Set.InvOn.bijOn setInvOn_digitsAppend_ofDigits mapsTo_ofDigits mapsTo_digitsAppend
bijOn_ofDigits' 📖	mathematical	—	Set.BijOn ofDigits instSemiring SetLike.coe Finset Finset.instSetLike List.fixedLengthDigits Finset.range Monoid.toNatPow instMonoid	—	mapsTo_ofDigits Set.coe_toFinset Set.ext Finset.coe_range bijOn_ofDigits
digits_append_digits 📖	mathematical	—	digits Monoid.toNatPow instMonoid	—	eq_or_lt_of_le zero_add one_pow one_mul ofDigits_digits_append_digits digits_ofDigits digits_lt_base getLast_digit_ne_zero digits_ne_nil_iff_ne_zero List.getLast_append_of_right_ne_nil
digits_append_zeroes_append_digits 📖	mathematical	—	digits Monoid.toNatPow instMonoid	—	digits_base_pow_mul digits_append_digits AddLeftCancelSemigroup.toIsLeftCancelAdd Mathlib.Tactic.Ring.of_eq 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.add_congr Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add
digits_len 📖	mathematical	—	digits log	—	strong_induction_on digits_eq_cons_digits_div digits_zero zero_add instCanonicallyOrderedAdd log_div_base tsub_add_cancel_of_le CanonicallyOrderedAdd.toExistsAddOfLE IsOrderedAddMonoid.toAddLeftMono instIsOrderedAddMonoid instOrderedSub log_pos Mathlib.Tactic.Contrapose.contrapose₂
digits_len_le_digits_len_succ 📖	mathematical	—	digits	—	Decidable.eq_or_ne digits_zero zero_add instCanonicallyOrderedAdd le_or_gt IsOrderedAddMonoid.toAddLeftMono instIsOrderedAddMonoid IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT AddLeftCancelSemigroup.toIsLeftCancelAdd contravariant_lt_of_covariant_le le_antisymm Mathlib.Tactic.IntervalCases.of_le_right Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.isNat_ofNat digits_zero_succ' digits_len covariant_swap_add_of_covariant_add IsRightCancelAdd.addRightReflectLE_of_addRightReflectLT AddRightCancelSemigroup.toIsRightCancelAdd contravariant_swap_add_of_contravariant_add log_mono_right
digits_length_le_iff 📖	mathematical	—	digits Monoid.toNatPow instMonoid	—	pow_pos IsStrictOrderedRing.toPosMulStrictMono instIsStrictOrderedRing IsStrictOrderedRing.toZeroLEOneClass lt_trans Mathlib.Meta.Positivity.pos_of_isNat IsStrictOrderedRing.toIsOrderedRing instNontrivial Mathlib.Meta.NormNum.isNat_ofNat digits_zero instCanonicallyOrderedAdd digits_len log_lt_iff_lt_pow
digits_two_eq_bits 📖	mathematical	—	digits bits	—	digits_zero zero_bits digits_of_two_le_of_pos instZeroLEOneClass one_bits bits_append_bit instAtLeastTwoHAddOfNat digits_def' one_lt_two IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd IsOrderedAddMonoid.toAddLeftMono instIsOrderedAddMonoid instCanonicallyOrderedAdd IsStrictOrderedRing.noZeroDivisors instIsStrictOrderedRing CanonicallyOrderedAdd.toExistsAddOfLE instCharZero mul_div_cancel_left₀ instMulDivCancelClass add_comm LinearOrderedCommMonoidWithZero.toPosMulStrictMono PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toIsOrderedRing instNontrivial add_zero
dvd_ofDigits_sub_ofDigits 📖	mathematical	semigroupDvd SemigroupWithZero.toSemigroup NonUnitalSemiring.toSemigroupWithZero NonUnitalCommSemiring.toNonUnitalSemiring NonUnitalCommRing.toNonUnitalCommSemiring CommRing.toNonUnitalCommRing SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne CommRing.toRing	ofDigits CommSemiring.toSemiring CommRing.toCommSemiring	—	sub_self add_sub_add_left_eq_sub dvd_mul_sub_mul
getD_digits 📖	mathematical	—	digits Monoid.toNatPow instMonoid	—	digits_zero instCanonicallyOrderedAdd List.head!_eq_head?_getD head!_digits pow_zero digits_of_two_le_of_pos covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono instIsOrderedAddMonoid IsRightCancelAdd.addRightReflectLE_of_addRightReflectLT AddRightCancelSemigroup.toIsRightCancelAdd contravariant_swap_add_of_contravariant_add contravariant_lt_of_covariant_le IsRightCancelAdd.addRightStrictMono_of_addRightMono instNoMaxOrder div_lt_self'
getLast_digit_ne_zero 📖	—	—	—	—	digits_ne_nil_iff_ne_zero zero_add List.getLast_replicate_succ digits_of_lt pos_iff_ne_zero instCanonicallyOrderedAdd digits_getLast Ne.bot_lt
head!_digits 📖	mathematical	—	digits	—	digits_zero ofDigits_digits ofDigits_mod_eq_head! digits_lt_base List.head!_mem_self digits_ne_nil_iff_ne_zero
injOn_ofDigits 📖	mathematical	—	Set.InjOn ofDigits instSemiring setOf	—	ofDigits_inj_of_len_eq
le_digits_len_le 📖	mathematical	—	digits	—	monotone_nat_of_le_succ digits_len_le_digits_len_succ
length_digitsAppend 📖	mathematical	Monoid.toNatPow instMonoid	digitsAppend	—	digits_length_le_iff
lt_digits_length_iff 📖	mathematical	—	digits Monoid.toNatPow instMonoid	—	Mathlib.Tactic.Contrapose.contrapose_iff₁ digits_length_le_iff
lt_of_mem_digitsAppend 📖	—	digitsAppend	—	—	digits_lt_base lt_of_not_ge Mathlib.Tactic.Linarith.lt_irrefl instAtLeastTwoHAddOfNat Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Tactic.Ring.neg_congr 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_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.add_pf_add_overlap Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.isNat_add Mathlib.Tactic.Ring.add_pf_zero_add 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_add_overlap_zero Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Ring.cast_zero Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Tactic.Linarith.add_lt_of_neg_of_le Int.instIsStrictOrderedRing Mathlib.Tactic.Linarith.mul_neg neg_neg_of_pos Int.instIsOrderedAddMonoid Mathlib.Tactic.Linarith.zero_lt_one Mathlib.Meta.NormNum.isNat_lt_true IsStrictOrderedRing.toIsOrderedRing Int.instCharZero Mathlib.Tactic.Linarith.sub_nonpos_of_le cast_one cast_zero
mapsTo_digitsAppend 📖	mathematical	—	Set.MapsTo digitsAppend setOf Monoid.toNatPow instMonoid	—	length_digitsAppend lt_of_mem_digitsAppend
mapsTo_ofDigits 📖	mathematical	—	Set.MapsTo ofDigits instSemiring setOf Monoid.toNatPow instMonoid	—	ofDigits_lt_base_pow_length Set.mem_setOf
modEq_digits_sum 📖	mathematical	—	ModEq MulZeroClass.toZero instMulZeroClass digits	—	ofDigits_one ofDigits_digits ofDigits_modEq
ofDigits_eq_sum_mapIdx 📖	mathematical	—	ofDigits instSemiring MulZeroClass.toZero instMulZeroClass Monoid.toNatPow instMonoid	—	ofDigits_eq_foldr pow_zero mul_one ofDigits_eq_sum_mapIdx_aux IsCancelMulZero.toIsLeftCancelMulZero instIsCancelMulZero
ofDigits_eq_sum_mapIdx_aux 📖	mathematical	—	MulZeroClass.toZero instMulZeroClass Monoid.toNatPow instMonoid	—	Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.pow_congr Mathlib.Tactic.Ring.add_congr 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 List.sum_zipWith_distrib_left
ofDigits_mod 📖	mathematical	—	ofDigits instSemiring	—	ofDigits_modEq
ofDigits_modEq 📖	mathematical	—	ModEq ofDigits instSemiring	—	ofDigits_modEq' ModEq.symm mod_modEq
ofDigits_modEq' 📖	mathematical	ModEq	ofDigits instSemiring	—	—
ofDigits_mod_eq_head! 📖	mathematical	—	ofDigits instSemiring	—	—
ofDigits_neg_one 📖	mathematical	—	ofDigits Int.instSemiring List.alternatingSum MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Int.instCommRing	—	MulZeroClass.mul_zero add_zero List.alternatingSum_cons sub_zero Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.mul_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.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.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.neg_mul
ofDigits_zmod 📖	mathematical	—	ofDigits Int.instSemiring	—	ofDigits_zmodeq
ofDigits_zmodeq 📖	mathematical	—	Int.ModEq ofDigits Int.instSemiring	—	ofDigits_zmodeq' Int.ModEq.symm Int.mod_modEq
ofDigits_zmodeq' 📖	mathematical	Int.ModEq	ofDigits Int.instSemiring	—	—
pow_length_le_mul_ofDigits 📖	mathematical	—	Monoid.toNatPow instMonoid ofDigits instSemiring	—	List.dropLast_append_getLast zero_add add_comm pow_add pow_one ofDigits_append ofDigits_singleton le_trans pos_iff_ne_zero instCanonicallyOrderedAdd
setInvOn_digitsAppend_ofDigits 📖	mathematical	—	Set.InvOn digitsAppend ofDigits instSemiring setOf Monoid.toNatPow instMonoid	—	injOn_ofDigits length_digitsAppend mapsTo_ofDigits lt_of_mem_digitsAppend ofDigits_append_replicate_zero ofDigits_digits
sub_one_mul_sum_div_pow_eq_sub_sum_digits 📖	mathematical	—	Finset.sum instAddCommMonoid Finset.range ofDigits instSemiring Monoid.toNatPow instMonoid MulZeroClass.toZero instMulZeroClass	—	trichotomous Finset.sum_congr Finset.sum_const_zero MulZeroClass.mul_zero tsub_self instCanonicallyOrderedAdd instOrderedSub self_div_pow_eq_ofDigits_drop digits_ofDigits Finset.sum_range_succ cast_id em add_zero Finset.sum_singleton Finset.sum_range_add_sum_Ico ofDigits.eq_1 Ico_succ_singleton Finset.sum_Ico_consecutive Finset.sum_Ico_add instIsOrderedCancelAddMonoid CanonicallyOrderedAdd.toExistsAddOfLE Ico_zero_eq_range mul_add Distrib.leftDistribClass Finset.range_one sum_le_ofDigits one_mul add_mul Distrib.rightDistribClass ofDigits_one one_pow Finset.sum_const Finset.card_range nsmul_eq_mul MulZeroClass.zero_mul zero_tsub zero_pow IsOrderedAddMonoid.toAddLeftMono instIsOrderedAddMonoid IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT AddLeftCancelSemigroup.toIsLeftCancelAdd contravariant_lt_of_covariant_le
sub_one_mul_sum_log_div_pow_eq_sub_sum_digits 📖	mathematical	—	Finset.sum instAddCommMonoid Finset.range log Monoid.toNatPow instMonoid MulZeroClass.toZero instMulZeroClass digits	—	trichotomous eq_or_ne Finset.sum_congr log_zero_right zero_add Finset.sum_const_zero MulZeroClass.mul_zero digits_zero tsub_self instCanonicallyOrderedAdd instOrderedSub digits_len ofDigits_digits sub_one_mul_sum_div_pow_eq_sub_sum_digits digits_ne_nil_iff_ne_zero getLast_digit_ne_zero digits_lt_base log_one_left one_pow Finset.sum_const Finset.card_singleton nsmul_eq_mul cast_one one_mul MulZeroClass.zero_mul List.sum_replicate mul_one zero_tsub log_zero_left zero_pow add_zero
sum_digits_ofDigits_eq_sum 📖	mathematical	Set Set.instMembership setOf	MulZeroClass.toZero instMulZeroClass digits ofDigits instSemiring	—	setInvOn_digitsAppend_ofDigits List.sum_replicate nsmul_zero add_zero
sum_sum_digits_eq 📖	mathematical	—	Finset.sum instAddCommMonoid Finset.range Monoid.toNatPow instMonoid MulZeroClass.toZero instMulZeroClass digits choose	—	List.sum_fixedLengthDigits_sum Finset.sum_nbij bijOn_ofDigits' sum_digits_ofDigits_eq_sum List.mem_fixedLengthDigits_iff
zmodeq_ofDigits_digits 📖	mathematical	Int.ModEq	ofDigits Int.instSemiring digits	—	ofDigits_digits coe_ofDigits ofDigits_zmodeq'

---

← Back to Index