lean_workbook_plus_5167

Proved

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

Example: $12\equiv5\pmod{7}$ is a true statement, because $7|12-5$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_5167 : 12 ≡ 5 [ZMOD 7]   :=  by sorry

Source