lean_workbook_plus_31269

Proved

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

Prove that each element $a$ in the set ${1, 2, 3, 4, 5, 6...p-2, p-1}$ has an inverse $b$ in the same set modulo $p$ , where $p$ is a prime number.

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_31269 (p : ℕ) (hp : p.Prime) (a : ZMod p) (ha : a ≠ 0) : ∃ b : ZMod p, a * b = 1   :=  by sorry

Source