Commit 2024-05-05 19:07 b41d4d86

View on Github →

feat(Nat/Digits): ofDigits_add_ofDigits_eq_ofDigits_zipWith_of_length_eq (#12642)

Estimated changes

Modified Mathlib/Data/Nat/Digits.lean

added theorem Nat.mul_ofDigits

added theorem Nat.ofDigits_add_ofDigits_eq_ofDigits_zipWith_of_length_eq

added theorem Nat.ofDigits_cons