sum_le_ofDigits — Mathlib

English

For any list L and base p ≥ 1, the sum of the digits of L is not larger than the value represented by ofDigits p L.

Русский

Для любого списка L и основания p ≥ 1 сумма цифр L не превосходит значения ofDigits p L.

LaTeX

$$$ \forall L:\mathrm{List}\ \mathbb{N},\ p\ge 1:\ \mathrm{sum}(L) \le \mathrm{ofDigits}(p,L) $$$

Lean4

theorem sum_le_ofDigits {p : ℕ} (L : List ℕ) (h : 1 ≤ p) : L.sum ≤ ofDigits p L :=
  (ofDigits_one L).symm ▸ ofDigits_monotone L h

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