modEq_digits_sum — Mathlib

English

If b' % b = 1, then n is congruent to the sum of the digits of n in base b' modulo b.

Русский

Если b' % b = 1, то n эквивалентно сумме цифр n в основание b' по модулю b.

LaTeX

$$$n \equiv (\operatorname{digits}(b',n)).\text{sum} \ [MOD\ b]$$$

Lean4

theorem modEq_digits_sum (b b' : ℕ) (h : b' % b = 1) (n : ℕ) : n ≡ (digits b' n).sum [MOD b] :=
  by
  rw [← ofDigits_one]
  conv =>
    congr
    · skip
    · rw [← ofDigits_digits b' n]
  convert ofDigits_modEq b' b (digits b' n)
  exact h.symm

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