Mathlib Changelog
Changelog
About
Github
Commit
2020-09-21 16:27
92c01257
View on Github →
chore(data/nat/digits): use nat namespace (
#4201
)
Estimated changes
Modified
docs/100.yaml
Modified
src/data/nat/digits.lean
deleted
theorem
base_pow_length_digits_le'
deleted
theorem
base_pow_length_digits_le
deleted
theorem
coe_int_of_digits
deleted
theorem
coe_of_digits
deleted
def
digits
deleted
theorem
digits_add
deleted
theorem
digits_add_two_add_one
deleted
def
digits_aux
deleted
def
digits_aux_0
deleted
def
digits_aux_1
deleted
theorem
digits_aux_def
deleted
theorem
digits_aux_zero
deleted
theorem
digits_eq_nil_iff_eq_zero
deleted
theorem
digits_last
deleted
theorem
digits_len_le_digits_len_succ
deleted
theorem
digits_lt_base'
deleted
theorem
digits_lt_base
deleted
theorem
digits_ne_nil_iff_ne_zero
deleted
theorem
digits_of_digits
deleted
theorem
digits_of_lt
deleted
theorem
digits_one
deleted
theorem
digits_one_succ
deleted
theorem
digits_zero
deleted
theorem
digits_zero_of_eq_zero
deleted
theorem
digits_zero_succ
deleted
theorem
digits_zero_zero
deleted
theorem
dvd_iff_dvd_digits_sum
deleted
theorem
dvd_iff_dvd_of_digits
deleted
theorem
dvd_of_digits_sub_of_digits
deleted
theorem
eleven_dvd_iff
deleted
theorem
last_digit_ne_zero
deleted
theorem
le_digits_len_le
deleted
theorem
lt_base_pow_length_digits'
deleted
theorem
lt_base_pow_length_digits
deleted
theorem
modeq_digits_sum
deleted
theorem
modeq_eleven_digits_sum
deleted
theorem
modeq_nine_digits_sum
deleted
theorem
modeq_three_digits_sum
added
theorem
nat.base_pow_length_digits_le'
added
theorem
nat.base_pow_length_digits_le
added
theorem
nat.coe_int_of_digits
added
theorem
nat.coe_of_digits
added
def
nat.digits
added
theorem
nat.digits_add
added
theorem
nat.digits_add_two_add_one
added
def
nat.digits_aux
added
def
nat.digits_aux_0
added
def
nat.digits_aux_1
added
theorem
nat.digits_aux_def
added
theorem
nat.digits_aux_zero
added
theorem
nat.digits_eq_nil_iff_eq_zero
added
theorem
nat.digits_last
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_of_digits
added
theorem
nat.digits_of_lt
added
theorem
nat.digits_one
added
theorem
nat.digits_one_succ
added
theorem
nat.digits_zero
added
theorem
nat.digits_zero_of_eq_zero
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_of_digits
added
theorem
nat.dvd_of_digits_sub_of_digits
added
theorem
nat.eleven_dvd_iff
added
theorem
nat.last_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.of_digits
added
theorem
nat.of_digits_append
added
theorem
nat.of_digits_digits
added
theorem
nat.of_digits_digits_append_digits
added
theorem
nat.of_digits_eq_foldr
added
theorem
nat.of_digits_lt_base_pow_length'
added
theorem
nat.of_digits_lt_base_pow_length
added
theorem
nat.of_digits_mod
added
theorem
nat.of_digits_modeq'
added
theorem
nat.of_digits_modeq
added
theorem
nat.of_digits_neg_one
added
theorem
nat.of_digits_one
added
theorem
nat.of_digits_one_cons
added
theorem
nat.of_digits_singleton
added
theorem
nat.of_digits_zmod
added
theorem
nat.of_digits_zmodeq'
added
theorem
nat.of_digits_zmodeq
added
theorem
nat.pow_length_le_mul_of_digits
added
theorem
nat.three_dvd_iff
added
theorem
nat.zmodeq_of_digits_digits
deleted
theorem
nine_dvd_iff
deleted
def
of_digits
deleted
theorem
of_digits_append
deleted
theorem
of_digits_digits
deleted
theorem
of_digits_digits_append_digits
deleted
theorem
of_digits_eq_foldr
deleted
theorem
of_digits_lt_base_pow_length'
deleted
theorem
of_digits_lt_base_pow_length
deleted
theorem
of_digits_mod
deleted
theorem
of_digits_modeq'
deleted
theorem
of_digits_modeq
deleted
theorem
of_digits_neg_one
deleted
theorem
of_digits_one
deleted
theorem
of_digits_one_cons
deleted
theorem
of_digits_singleton
deleted
theorem
of_digits_zmod
deleted
theorem
of_digits_zmodeq'
deleted
theorem
of_digits_zmodeq
deleted
theorem
pow_length_le_mul_of_digits
deleted
theorem
three_dvd_iff
deleted
theorem
zmodeq_of_digits_digits