Commit 2025-06-19 14:15 cd0260d1

View on Github →

chore: split Data.Nat.Digits (#26134) I noticed Mathlib.Data.List.Palindrome being built on the way to something that really shouldn't have needed it, and decided to stomp on it.

Estimated changes

deleted theorem Nat.digits_append_digits
deleted theorem Nat.digits_len
deleted theorem Nat.digits_two_eq_bits
deleted theorem Nat.dvd_iff_dvd_ofDigits
deleted theorem Nat.eleven_dvd_iff
deleted theorem Nat.getLast_digit_ne_zero
deleted theorem Nat.head!_digits
deleted theorem Nat.le_digits_len_le
deleted theorem Nat.modEq_digits_sum
deleted theorem Nat.modEq_nine_digits_sum
deleted theorem Nat.nine_dvd_iff
deleted theorem Nat.ofDigits_mod
deleted theorem Nat.ofDigits_modEq'
deleted theorem Nat.ofDigits_modEq
deleted theorem Nat.ofDigits_mod_eq_head!
deleted theorem Nat.ofDigits_neg_one
deleted theorem Nat.ofDigits_zmod
deleted theorem Nat.ofDigits_zmodeq'
deleted theorem Nat.ofDigits_zmodeq
deleted theorem Nat.three_dvd_iff
added theorem Nat.eleven_dvd_iff
added theorem Nat.nine_dvd_iff
added theorem Nat.three_dvd_iff
added theorem Nat.digits_len
added theorem Nat.digits_two_eq_bits
added theorem Nat.head!_digits
added theorem Nat.le_digits_len_le
added theorem Nat.modEq_digits_sum
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_zmod
added theorem Nat.ofDigits_zmodeq'
added theorem Nat.ofDigits_zmodeq