modEq_eleven_digits_sum — Mathlib

English

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

Русский

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

LaTeX

$$$\\forall n\\in\\mathbb{N},\\ n \\equiv \\big( (\\mathrm{digits}\\ 10\\ n).map (\\lambda d:\\mathbb{Z}.d) \\big).alternatingSum \\pmod{11}$$$

Lean4

theorem modEq_eleven_digits_sum (n : ℕ) : n ≡ ((digits 10 n).map fun n : ℕ => (n : ℤ)).alternatingSum [ZMOD 11] :=
  by
  have t := zmodeq_ofDigits_digits 11 10 (-1 : ℤ) (by unfold Int.ModEq; rfl) n
  rwa [ofDigits_neg_one] at t

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