Commit 2020-09-21 16:27 92c01257

View on Github →

chore(data/nat/digits): use nat namespace (#4201)

Estimated changes

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_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 eleven_dvd_iff
deleted theorem last_digit_ne_zero
deleted theorem le_digits_len_le
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.coe_int_of_digits
added theorem nat.coe_of_digits
added def nat.digits
added theorem nat.digits_add
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_last
added theorem nat.digits_lt_base'
added theorem nat.digits_lt_base
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_succ
added theorem nat.digits_zero_zero
added theorem nat.eleven_dvd_iff
added theorem nat.last_digit_ne_zero
added theorem nat.le_digits_len_le
added theorem nat.modeq_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_eq_foldr
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_zmod
added theorem nat.of_digits_zmodeq'
added theorem nat.of_digits_zmodeq
added theorem nat.three_dvd_iff
deleted theorem nine_dvd_iff
deleted def of_digits
deleted theorem of_digits_append
deleted theorem of_digits_digits
deleted theorem of_digits_eq_foldr
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 three_dvd_iff
deleted theorem zmodeq_of_digits_digits