modEq_nine_digits_sum — Mathlib

English

For every natural n, n is congruent modulo 9 to the sum of its decimal digits.

Русский

Для каждого натурального n выполняется равенство по модулю 9: n равно сумме десятичных цифр.

LaTeX

$$$\\forall n\\in\\mathbb{N},\\ n \\equiv (\\mathrm{digits}\\ 10\\ n).sum \\pmod{9}$$$

Lean4

theorem modEq_nine_digits_sum (n : ℕ) : n ≡ (digits 10 n).sum [MOD 9] :=
  modEq_digits_sum 9 10 (by simp) n

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