Theorem Nat.sub_one_mul_sum_div_pow_eq_sub_sum_digits

Modification history

2024-04-14 10:41
Mathlib/Data/Nat/Digits.lean
chore: remove autoImplicit from more files (#11798) …
Modified Nat.sub_one_mul_sum_div_pow_eq_sub_sum_digitsView on Github →
2023-08-11 15:25
Mathlib/Data/Nat/Digits.lean
feat(Data/Nat/Digits): sub_one_mul_sum_div_pow_eq_sub_sum_digits (#6505) …
Added Nat.sub_one_mul_sum_div_pow_eq_sub_sum_digitsView on Github →