nine_dvd_iff

Mathlib.Data.Nat.Digits.Div

URI: https://scilib.ai/kg/mathlib#Nat.nine_dvd_iff

English

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

Русский

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

LaTeX

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

Lean4

theorem nine_dvd_iff (n : ℕ) : 9 ∣ n ↔ 9 ∣ (digits 10 n).sum :=
  dvd_iff_dvd_digits_sum 9 10 (by simp) n

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru