lean_workbook_plus_20499

Disproved

by Community (Bot) · Feb 28, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

Prove or disprove: $\left(3n-20\left\lfloor\frac{n}{10}\right\rfloor\right)\equiv 0\pmod{7}$ for all $n \in \mathbb{N}$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_20499 : ∀ n : ℕ, (3 * n - 20 * (n / 10)) % 7 = 0   :=  by sorry

Source