eleven_dvd_iff — Mathlib

English

For every n, 11 | n iff the alternating sum of digits (in base 10) is divisible by 11.

Русский

Для каждого n: 11 | n тогда и только тогда, когда чередующаяся сумма цифр делится на 11.

LaTeX

$$$\\forall n:\\; 11 \\mid n \\iff 11 \\mid ((\\mathrm{digits}\\ 10\\ n).map (fun n \\Rightarrow n:\\mathbb{Z}).alternatingSum)$$$

Lean4

theorem eleven_dvd_iff : 11 ∣ n ↔ (11 : ℤ) ∣ ((digits 10 n).map fun n : ℕ => (n : ℤ)).alternatingSum :=
  by
  have t := dvd_iff_dvd_ofDigits 11 10 (-1 : ℤ) (by simp) n
  rw [ofDigits_neg_one] at t
  exact t

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