Defs

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

Statistics

Metric	Count
Definitions digits, digitsAux, digitsAux0, digitsAux1, ofDigits	5
Theorems coe_ofDigits, digit_sum_le, injective, digitsAux_def, digitsAux_zero, digits_add, digits_add_two_add_one, digits_base_mul, digits_base_pow_mul, digits_def', digits_eq_cons_digits_div, digits_eq_nil_iff_eq_zero, digits_getLast, digits_inj_iff, digits_lt_base, digits_lt_base', digits_ne_nil_iff_ne_zero, digits_ofDigits, digits_of_lt, digits_of_two_le_of_pos, digits_one, digits_one_succ, digits_zero, digits_zero_of_eq_zero, digits_zero_succ, digits_zero_succ', digits_zero_zero, lt_base_pow_length_digits, lt_base_pow_length_digits', mul_ofDigits, nat_repr_len_aux, ofDigits_add_ofDigits_eq_ofDigits_zipWith_of_length_eq, ofDigits_append, ofDigits_append_replicate_zero, ofDigits_append_zero, ofDigits_cons, ofDigits_digits, ofDigits_digits_append_digits, ofDigits_div_eq_ofDigits_tail, ofDigits_div_pow_eq_ofDigits_drop, ofDigits_eq_foldr, ofDigits_inj_of_len_eq, ofDigits_lt_base_pow_length, ofDigits_lt_base_pow_length', ofDigits_mod_pow_eq_ofDigits_take, ofDigits_monotone, ofDigits_nil, ofDigits_one, ofDigits_one_cons, ofDigits_replicate_zero, ofDigits_reverse_cons, ofDigits_reverse_zero_cons, ofDigits_singleton, repr_length, self_div_pow_eq_ofDigits_drop, self_mod_pow_eq_ofDigits_take, sum_le_ofDigits, toDigitsCore_length, toDigitsCore_lens_eq, toDigitsCore_lens_eq_aux, toDigits_length	61
Total	66

Nat

Definitions

Name	Category	Theorems
digits 📖	CompOp	57 math math: digits_zero_succ', sub_one_mul_sum_log_div_pow_eq_sub_sum_digits, digits_len_le_digits_len_succ, digits_len, getD_digits, digits_of_two_le_of_pos, sub_one_mul_padicValNat_factorial, modEq_digits_sum, digits_zero_succ, sub_one_mul_padicValNat_choose_eq_sub_sum_digits, digits_one, ofDigits_digits_append_digits, three_dvd_iff, sub_one_mul_padicValNat_choose_eq_sub_sum_digits', digits_add_two_add_one, digits_add, nine_dvd_iff, le_digits_len_le, digits_append_digits, digits_eq_nil_iff_eq_zero, sum_digits_ofDigits_eq_sum, dvd_iff_dvd_digits_sum, lt_base_pow_length_digits', base_pow_length_digits_le', digits_zero_zero, digits_one_succ, digits_length_le_iff, digits_zero, lt_digits_length_iff, digits_base_mul, digit_sum_le, digits_def', digits_of_lt, digits_ofDigits, dvd_iff_dvd_ofDigits, sub_one_mul_factorization_factorial, modEq_eleven_digits_sum, sum_sum_digits_eq, modEq_three_digits_sum, digits_eq_cons_digits_div, lt_base_pow_length_digits, digits_inj_iff, head!_digits, zmodeq_ofDigits_digits, self_mod_pow_eq_ofDigits_take, base_pow_length_digits_le, modEq_nine_digits_sum, digits_getLast, digits.injective, digits_two_eq_bits, digits_base_pow_mul, Rat.AbsoluteValue.apply_le_sum_digits, digits_append_zeroes_append_digits, Prime.sub_one_mul_multiplicity_factorial, self_div_pow_eq_ofDigits_drop, ofDigits_digits, eleven_dvd_iff
digitsAux 📖	CompOp	2 math math: digitsAux_zero, digitsAux_def
digitsAux0 📖	CompOp	—
digitsAux1 📖	CompOp	—
ofDigits 📖	CompOp	47 math math: ofDigits_zmodeq, ofDigits_lt_base_pow_length, ofDigits_one, sum_le_ofDigits, ofDigits_lt_base_pow_length', ofDigits_eq_sum_mapIdx, ofDigits_append_zero, ofDigits_digits_append_digits, ofDigits_mod_pow_eq_ofDigits_take, pow_length_le_mul_ofDigits, ofDigits_one_cons, bijOn_ofDigits, injOn_ofDigits, ofDigits_mod_eq_head!, ofDigits_div_pow_eq_ofDigits_drop, bijOn_ofDigits', ofDigits_monotone, ofDigits_replicate_zero, ofDigits_eq_foldr, ofDigits_cons, sum_digits_ofDigits_eq_sum, ofDigits_nil, ofDigits_reverse_cons, coe_ofDigits, ofDigits_mod, setInvOn_digitsAppend_ofDigits, ofDigits_zmodeq', ofDigits_append, sub_one_mul_sum_div_pow_eq_sub_sum_digits, digits_ofDigits, dvd_iff_dvd_ofDigits, ofDigits_singleton, ofDigits_reverse_zero_cons, ofDigits_append_replicate_zero, ofDigits_neg_one, zmodeq_ofDigits_digits, self_mod_pow_eq_ofDigits_take, ofDigits_add_ofDigits_eq_ofDigits_zipWith_of_length_eq, ofDigits_modEq, ofDigits_modEq', mul_ofDigits, ofDigits_div_eq_ofDigits_tail, dvd_ofDigits_sub_ofDigits, self_div_pow_eq_ofDigits_drop, mapsTo_ofDigits, ofDigits_digits, ofDigits_zmod

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coe_ofDigits 📖	mathematical	—	AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring ofDigits instSemiring	—	cast_zero cast_add cast_mul
digit_sum_le 📖	mathematical	—	MulZeroClass.toZero instMulZeroClass digits	—	digits_zero digits_zero_succ add_zero le_refl ofDigits_digits ofDigits_one ofDigits_monotone
digitsAux_def 📖	mathematical	—	digitsAux	—	digitsAux.eq_2
digitsAux_zero 📖	mathematical	—	digitsAux	—	—
digits_add 📖	mathematical	—	digits	—	MulZeroClass.mul_zero add_zero digits_of_lt digits_zero digitsAux_def IsRightCancelAdd.addRightStrictMono_of_addRightMono AddRightCancelSemigroup.toIsRightCancelAdd covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono instIsOrderedAddMonoid contravariant_swap_add_of_contravariant_add contravariant_lt_of_covariant_le instCanonicallyOrderedAdd IsStrictOrderedRing.toIsOrderedRing instIsStrictOrderedRing instNontrivial instAtLeastTwoHAddOfNat zero_add
digits_add_two_add_one 📖	mathematical	—	digits	—	digitsAux_def IsRightCancelAdd.addRightStrictMono_of_addRightMono AddRightCancelSemigroup.toIsRightCancelAdd covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono instIsOrderedAddMonoid contravariant_swap_add_of_contravariant_add contravariant_lt_of_covariant_le instCanonicallyOrderedAdd instZeroLEOneClass
digits_base_mul 📖	mathematical	—	digits	—	digits_def' mul_pos LinearOrderedCommMonoidWithZero.toPosMulStrictMono lt_trans Mathlib.Meta.Positivity.pos_of_isNat IsStrictOrderedRing.toIsOrderedRing instIsStrictOrderedRing instNontrivial Mathlib.Meta.NormNum.isNat_ofNat
digits_base_pow_mul 📖	mathematical	—	digits Monoid.toNatPow instMonoid	—	pow_zero one_mul mul_assoc digits_base_mul mul_pos LinearOrderedCommMonoidWithZero.toPosMulStrictMono pow_pos IsStrictOrderedRing.toPosMulStrictMono instIsStrictOrderedRing IsStrictOrderedRing.toZeroLEOneClass lt_trans Mathlib.Meta.Positivity.pos_of_isNat IsStrictOrderedRing.toIsOrderedRing instNontrivial Mathlib.Meta.NormNum.isNat_ofNat
digits_def' 📖	mathematical	—	digits	—	digitsAux_def 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 instCanonicallyOrderedAdd
digits_eq_cons_digits_div 📖	mathematical	—	digits	—	digits_def'
digits_eq_nil_iff_eq_zero 📖	mathematical	—	digits	—	ofDigits_digits digits_zero
digits_getLast 📖	mathematical	—	digits	—	digits_zero digits_eq_cons_digits_div
digits_inj_iff 📖	mathematical	—	digits	—	digits.injective
digits_lt_base 📖	—	digits	—	—	instCanonicallyOrderedAdd zero_add digits_lt_base'
digits_lt_base' 📖	—	digits	—	—	digits_zero digits_add_two_add_one 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.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_gt 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 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 Mathlib.Tactic.Linarith.natCast_nonneg cast_add cast_zero
digits_ne_nil_iff_ne_zero 📖	—	—	—	—	digits_eq_nil_iff_eq_zero
digits_ofDigits 📖	mathematical	—	digits ofDigits instSemiring	—	digits_zero digits_add Mathlib.Tactic.Contrapose.contrapose₄ digits_zero_of_eq_zero LT.lt.ne_bot
digits_of_lt 📖	mathematical	—	digits	—	LE.le.trans_lt digits_add_two_add_one digits_zero
digits_of_two_le_of_pos 📖	mathematical	—	digits	—	digits_add_two_add_one
digits_one 📖	mathematical	—	digits	—	—
digits_one_succ 📖	mathematical	—	digits	—	—
digits_zero 📖	mathematical	—	digits	—	—
digits_zero_of_eq_zero 📖	—	ofDigits instSemiring	—	—	mul_right_injective₀ IsCancelMulZero.toIsLeftCancelMulZero instIsCancelMulZero
digits_zero_succ 📖	mathematical	—	digits	—	—
digits_zero_succ' 📖	mathematical	—	digits	—	—
digits_zero_zero 📖	mathematical	—	digits	—	—
lt_base_pow_length_digits 📖	mathematical	—	Monoid.toNatPow instMonoid digits	—	instCanonicallyOrderedAdd zero_add lt_base_pow_length_digits'
lt_base_pow_length_digits' 📖	mathematical	—	Monoid.toNatPow instMonoid digits	—	ofDigits_digits ofDigits_lt_base_pow_length' digits_lt_base'
mul_ofDigits 📖	mathematical	—	ofDigits instSemiring	—	ofDigits_cons Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_left 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.zero_mul Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add
nat_repr_len_aux 📖	—	Monoid.toNatPow instMonoid	—	—	—
ofDigits_add_ofDigits_eq_ofDigits_zipWith_of_length_eq 📖	mathematical	—	ofDigits instSemiring	—	add_zero AddRightCancelSemigroup.toIsRightCancelAdd mul_add Distrib.leftDistribClass
ofDigits_append 📖	mathematical	—	ofDigits instSemiring Monoid.toNatPow instMonoid	—	pow_zero one_mul zero_add ofDigits.eq_2 Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.mul_congr 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_gt Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add
ofDigits_append_replicate_zero 📖	mathematical	—	ofDigits instSemiring	—	ofDigits_append ofDigits_replicate_zero MulZeroClass.mul_zero add_zero
ofDigits_append_zero 📖	mathematical	—	ofDigits instSemiring	—	ofDigits_append ofDigits_singleton MulZeroClass.mul_zero add_zero
ofDigits_cons 📖	mathematical	—	ofDigits instSemiring	—	—
ofDigits_digits 📖	mathematical	—	ofDigits instSemiring digits	—	ofDigits_singleton ofDigits_one_cons add_comm digits_zero digits_add_two_add_one div_lt_self'
ofDigits_digits_append_digits 📖	mathematical	—	ofDigits instSemiring digits Monoid.toNatPow instMonoid	—	ofDigits_append ofDigits_digits
ofDigits_div_eq_ofDigits_tail 📖	mathematical	—	ofDigits instSemiring	—	zero_add
ofDigits_div_pow_eq_ofDigits_drop 📖	mathematical	—	ofDigits instSemiring Monoid.toNatPow instMonoid	—	pow_zero ofDigits_div_eq_ofDigits_tail add_comm
ofDigits_eq_foldr 📖	mathematical	—	ofDigits Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Distrib.toMul MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass	—	—
ofDigits_inj_of_len_eq 📖	—	ofDigits instSemiring	—	—	AddRightCancelSemigroup.toIsRightCancelAdd AddLeftCancelSemigroup.toIsLeftCancelAdd mul_left_cancel_iff_of_pos PosMulStrictMono.toPosMulReflectLE LinearOrderedCommMonoidWithZero.toPosMulStrictMono
ofDigits_lt_base_pow_length 📖	mathematical	—	ofDigits instSemiring Monoid.toNatPow instMonoid	—	instCanonicallyOrderedAdd zero_add ofDigits_lt_base_pow_length'
ofDigits_lt_base_pow_length' 📖	mathematical	—	ofDigits instSemiring Monoid.toNatPow instMonoid	—	pow_zero instZeroLEOneClass ofDigits.eq_2 pow_succ mul_le_mul IsOrderedRing.toPosMulMono IsStrictOrderedRing.toIsOrderedRing instIsStrictOrderedRing IsOrderedRing.toMulPosMono le_refl lt_of_not_ge Mathlib.Tactic.Linarith.lt_irrefl instAtLeastTwoHAddOfNat 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.mul_congr Mathlib.Tactic.Ring.atom_pf 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.one_mul Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.pow_congr Mathlib.Tactic.Ring.pow_add Mathlib.Tactic.Ring.pow_atom Mathlib.Tactic.Ring.pow_zero Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_mul Mathlib.Tactic.Ring.add_pf_add_overlap Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Tactic.Ring.mul_one Mathlib.Tactic.Ring.cast_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 cast_mul cast_add coe_ofDigits cast_one cast_pow
ofDigits_mod_pow_eq_ofDigits_take 📖	mathematical	—	ofDigits instSemiring Monoid.toNatPow instMonoid	—	pow_zero ofDigits_cons lt_of_lt_of_le pow_pos LinearOrderedCommMonoidWithZero.toPosMulStrictMono instZeroLEOneClass
ofDigits_monotone 📖	mathematical	—	ofDigits instSemiring	—	le_refl IsOrderedAddMonoid.toAddLeftMono instIsOrderedAddMonoid IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT AddLeftCancelSemigroup.toIsLeftCancelAdd contravariant_lt_of_covariant_le
ofDigits_nil 📖	mathematical	—	ofDigits instSemiring	—	—
ofDigits_one 📖	mathematical	—	ofDigits instSemiring MulZeroClass.toZero instMulZeroClass	—	one_mul
ofDigits_one_cons 📖	mathematical	—	ofDigits AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring AddMonoidWithOne.toNatCast	—	one_mul
ofDigits_replicate_zero 📖	mathematical	—	ofDigits instSemiring	—	MulZeroClass.mul_zero add_zero
ofDigits_reverse_cons 📖	mathematical	—	ofDigits instSemiring Monoid.toNatPow instMonoid	—	ofDigits_append ofDigits_singleton
ofDigits_reverse_zero_cons 📖	mathematical	—	ofDigits instSemiring	—	ofDigits_append_zero
ofDigits_singleton 📖	mathematical	—	ofDigits instSemiring	—	MulZeroClass.mul_zero add_zero
repr_length 📖	—	Monoid.toNatPow instMonoid	—	—	toDigits_length
self_div_pow_eq_ofDigits_drop 📖	mathematical	—	Monoid.toNatPow instMonoid ofDigits instSemiring digits	—	ofDigits_digits ofDigits_div_pow_eq_ofDigits_drop digits_lt_base
self_mod_pow_eq_ofDigits_take 📖	mathematical	—	Monoid.toNatPow instMonoid ofDigits instSemiring digits	—	ofDigits_digits ofDigits_mod_pow_eq_ofDigits_take digits_lt_base
sum_le_ofDigits 📖	mathematical	—	MulZeroClass.toZero instMulZeroClass ofDigits instSemiring	—	ofDigits_monotone ofDigits_one
toDigitsCore_length 📖	—	Monoid.toNatPow instMonoid	—	—	pow_one zero_add instCanonicallyOrderedAdd toDigitsCore_lens_eq
toDigitsCore_lens_eq 📖	—	—	—	—	—
toDigitsCore_lens_eq_aux 📖	—	—	—	—	—
toDigits_length 📖	—	Monoid.toNatPow instMonoid	—	—	toDigitsCore_length

Nat.digits

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
injective 📖	mathematical	—	Nat.digits	—	Nat.ofDigits_digits

---

← Back to Index