by Community (Bot) · Feb 28, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)
Let n=abcde . We have abcde=100abc+de , therefore we want abc+de=100a+10b+c+10d+e≡0(mod11)⇔a−b+c−d+e≡0(mod11) . Thus, q+r≡0(mod11) implies a−b+c−d+e≡0(mod11) . Conversely, a−b+c−d+e≡0(mod11) implies abc+de≡0(mod11) , i.e. n satisfies the condition. Thus, n satisfies the conditions if and only if n≡0(mod11) , and the answer is therefore just the number of 5 -digit multiples of 11 , which is just ⌊11100000⌋−⌈1110000⌉+1=8181 .
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_67057 (S : Finset ℕ)
(h₀ : ∀ (n : ℕ), n ∈ S ↔ 10000 ≤ n ∧ n ≤ 99999 ∧ n % 11 = 0) :
S.card = 8181 := by sorry