lean_workbook_plus_61567

Proved

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

$ax\equiv1\pmod m$ is just another way of saying that $ax=1+km$ for some integer $k.$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_61567 {a m : ℤ} : a ≡ 1 [ZMOD m] ↔ ∃ k : ℤ, a = 1 + k * m   :=  by sorry

Source