Commit 2024-11-28 13:58 63a0f6a0

feat: add Nat.digits_base_pow_mul and Nat.digits_append_zeroes_append_digits (#19179) Adds two Nat.digits lemmas that I needed in Compfiles for USAMO 1992 Problem 1: https://github.com/dwrensha/compfiles/blob/472f49e2b567e05c2cc1d963d5efbd6118f2b66c/Compfiles/Usa1992P1.lean#L32-L52 Nat.digits_base_pow_mul is like Nat.digits_append_digits, but with Nat.digits b n replaced by List.replicate k 0. This new lemma is useful because Nat.digits b n can never equal a nonempty list of all zeroes. Nat.digits_append_zeroes_append_digits is like Nat.digits_append_digits with an extra List.replicate k 0 inserted in the middle.