Commit 2023-03-01 18:09 3b6aa733

View on Github →

feat: port Data.Nat.Digits (#2300)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Data/Nat/Digits.lean

added theorem Nat.NormDigits.digits_one

added theorem Nat.NormDigits.digits_succ

added theorem Nat.base_pow_length_digits_le'

added theorem Nat.base_pow_length_digits_le

added theorem Nat.coe_int_ofDigits

added theorem Nat.coe_ofDigits

added theorem Nat.digits.injective

added def Nat.digits

added def Nat.digitsAux0

added def Nat.digitsAux1

added def Nat.digitsAux

added theorem Nat.digitsAux_def

added theorem Nat.digitsAux_zero

added theorem Nat.digits_add

added theorem Nat.digits_add_two_add_one

added theorem Nat.digits_def'

added theorem Nat.digits_eq_cons_digits_div

added theorem Nat.digits_eq_nil_iff_eq_zero

added theorem Nat.digits_getLast

added theorem Nat.digits_inj_iff

added theorem Nat.digits_len

added theorem Nat.digits_len_le_digits_len_succ

added theorem Nat.digits_lt_base'

added theorem Nat.digits_lt_base

added theorem Nat.digits_ne_nil_iff_ne_zero

added theorem Nat.digits_ofDigits

added theorem Nat.digits_of_lt

added theorem Nat.digits_one

added theorem Nat.digits_one_succ

added theorem Nat.digits_two_eq_bits

added theorem Nat.digits_zero

added theorem Nat.digits_zero_of_eq_zero

added theorem Nat.digits_zero_succ'

added theorem Nat.digits_zero_succ

added theorem Nat.digits_zero_zero

added theorem Nat.dvd_iff_dvd_digits_sum

added theorem Nat.dvd_iff_dvd_ofDigits

added theorem Nat.dvd_ofDigits_sub_ofDigits

added theorem Nat.eleven_dvd_iff

added theorem Nat.eleven_dvd_of_palindrome

added theorem Nat.getLast_digit_ne_zero

added theorem Nat.le_digits_len_le

added theorem Nat.lt_base_pow_length_digits'

added theorem Nat.lt_base_pow_length_digits

added theorem Nat.modEq_digits_sum

added theorem Nat.modEq_eleven_digits_sum

added theorem Nat.modEq_nine_digits_sum

added theorem Nat.modEq_three_digits_sum

added theorem Nat.nine_dvd_iff

added def Nat.ofDigits

added theorem Nat.ofDigits_append

added theorem Nat.ofDigits_digits

added theorem Nat.ofDigits_digits_append_digits

added theorem Nat.ofDigits_eq_foldr

added theorem Nat.ofDigits_eq_sum_mapIdx

added theorem Nat.ofDigits_eq_sum_map_with_index_aux

added theorem Nat.ofDigits_lt_base_pow_length'

added theorem Nat.ofDigits_lt_base_pow_length

added theorem Nat.ofDigits_mod

added theorem Nat.ofDigits_modEq

added theorem Nat.ofDigits_modeq'

added theorem Nat.ofDigits_neg_one

added theorem Nat.ofDigits_one

added theorem Nat.ofDigits_one_cons

added theorem Nat.ofDigits_singleton

added theorem Nat.ofDigits_zmod

added theorem Nat.ofDigits_zmodeq'

added theorem Nat.ofDigits_zmodeq

added theorem Nat.pow_length_le_mul_ofDigits

added theorem Nat.three_dvd_iff

added theorem Nat.zmodeq_ofDigits_digits