Theorem Nat.ofDigits_div_pow_eq_ofDigits_drop

Modification history

2023-08-10 19:52
Mathlib/Data/Nat/Digits.lean
feat(Data/Nat/Digits): dividing by `p^i` (#6448)
Added Nat.ofDigits_div_pow_eq_ofDigits_dropView on Github →