Mathlib v3 is deprecated. Go to Mathlib v4

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