Commit 2023-09-08 11:01 20aad7f9

View on Github →

feat: add Nat.digits_append_digits (#6999) Similar to Nat.ofDigits_digits_append_digits, but with a digits on the RHS instead of an ofDigits on the LHS.

Estimated changes

Modified Mathlib/Data/Nat/Digits.lean

added theorem Nat.digits_append_digits