lean_workbook_plus_19085

Proved

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

Find all integers $x$ with $2\le x\le 199$ such that $x^3\equiv 1\pmod{199}$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_19085 (x : ℤ) (hx: 2 ≤ x ∧ x ≤ 199) (h : x^3 ≡ 1 [ZMOD 199]) : x = 92 ∨ x = 106   :=  by sorry

Source