n✝ b b' : ℕ
h : b' % b = 1
n : ℕ
⊢ b ∣ n ↔ b ∣ ofDigits 1 (digits b' n)
n✝ b b' : ℕ
h : b' % b = 1
n : ℕ
⊢ b ∣ n ↔ b ∣ List.sum (digits b' n)
rw [← ofDigits_one]
n✝ b b' : ℕ
h : b' % b = 1
n : ℕ
⊢ b ∣ ofDigits b' (digits b' n) ↔ b ∣ ofDigits 1 (digits b' n)
n✝ b b' : ℕ
h : b' % b = 1
n : ℕ
⊢ b ∣ n ↔ b ∣ ofDigits 1 (digits b' n)
conv_lhs => rw [← ofDigits_digits b' n]
no goals
n✝ b b' : ℕ
h : b' % b = 1
n : ℕ
⊢ b ∣ ofDigits b' (digits b' n) ↔ b ∣ ofDigits 1 (digits b' n)
rw [Nat.dvd_iff_mod_eq_zero, Nat.dvd_iff_mod_eq_zero, ofDigits_mod, h]