Divisibility_by_9
Proveddivisibility-by-9divisibility-testsproofwikiretry
A number is divisible by 9 iff the sum of its digits is divisible by 9.
Preamble
import Mathlib.Data.List.Basic import Mathlib.Data.Nat.GCD.Basic
Formal statement
theorem Divisibility_by_9 (digits : List ℕ) (h : ∀ d ∈ digits, d < 10) : 9 ∣ digits.foldr (fun d acc => d + 10 * acc) 0 ↔ 9 ∣ digits.sum := by sorry