English
Let b,b' be natural numbers, c an integer, and h:(b:Z) | (b':Z) - c. For any n, b | n iff (b:Z) | ofDigits c (digits b' n).
Русский
Пусть b, b' — натуральные числа, c — целое число, и (b:ℤ) делит (b':ℤ) - c. Тогда для любого n выполняется: b делит n тогда и только тогда, когда (b:ℤ) делит ofDigits c (digits b' n).
LaTeX
$$$\\forall b,b'\\in\\mathbb{N},\\ c\\in\\mathbb{Z},\\ h:(b:\\mathbb{Z}) \\mid (b':\\mathbb{Z})-c,\\ n\\in\\mathbb{N},\\ b \\mid n \\iff (b:\\mathbb{Z}) \\mid \\mathrm{ofDigits}\\ c (\\mathrm{digits}\\ b'\\ n)$$$
Lean4
theorem dvd_iff_dvd_digits_sum (b b' : ℕ) (h : b' % b = 1) (n : ℕ) : b ∣ n ↔ b ∣ (digits b' n).sum :=
by
rw [← ofDigits_one]
conv_lhs => rw [← ofDigits_digits b' n]
rw [Nat.dvd_iff_mod_eq_zero, Nat.dvd_iff_mod_eq_zero, ofDigits_mod, h]
