dvd_iff_dvd_ofDigits — Mathlib

English

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

Русский

Для любого n: 11 делит n тогда, когда чередующаяся сумма цифр записи числа по основанию 10 делится на 11.

LaTeX

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

Lean4

theorem dvd_iff_dvd_ofDigits (b b' : ℕ) (c : ℤ) (h : (b : ℤ) ∣ (b' : ℤ) - c) (n : ℕ) :
    b ∣ n ↔ (b : ℤ) ∣ ofDigits c (digits b' n) :=
  by
  rw [← Int.natCast_dvd_natCast]
  exact dvd_iff_dvd_of_dvd_sub (zmodeq_ofDigits_digits b b' c (Int.modEq_iff_dvd.2 h).symm _).symm.dvd

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