modEq_three_digits_sum — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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