Commit 2023-08-11 15:25 a71e9581

View on Github →

feat(Data/Nat/Digits): sub_one_mul_sum_div_pow_eq_sub_sum_digits (#6505)

depends on: #6448
depends on: #6493

Estimated changes

Modified Mathlib/Data/Nat/Digits.lean

added theorem Nat.sub_one_mul_sum_div_pow_eq_sub_sum_digits

added theorem Nat.sub_one_mul_sum_log_div_pow_eq_sub_sum_digits