three_dvd_iff — Mathlib

English

For every natural n, 3 | n iff 3 | (digits 10 n).sum.

Русский

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

LaTeX

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

Lean4

/-- **Divisibility by 3 Rule** -/
theorem three_dvd_iff (n : ℕ) : 3 ∣ n ↔ 3 ∣ (digits 10 n).sum :=
  dvd_iff_dvd_digits_sum 3 10 (by simp) n

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