digit_sum_le — Mathlib

English

For any p,n, the sum of the digits of n in base p is at most n.

Русский

Для любых p,n сумма цифр числа n в основании p не превышает самого n.

LaTeX

$$$ \forall p,n:\ \mathrm{sum}(\mathrm{digits}(p,n)) \le n $$$

Lean4

theorem digit_sum_le (p n : ℕ) : List.sum (digits p n) ≤ n := by
  induction n with
  | zero => exact digits_zero _ ▸ Nat.le_refl (List.sum [])
  | succ n =>
    induction p with
    | zero => rw [digits_zero_succ, List.sum_cons, List.sum_nil, add_zero]
    | succ p =>
      nth_rw 2 [← ofDigits_digits p.succ (n + 1)]
      rw [← ofDigits_one <| digits p.succ n.succ]
      exact ofDigits_monotone (digits p.succ n.succ) <| Nat.succ_pos p

Похожие утверждения