lean_workbook_plus_50222

Proved

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

It follows that $3^c \equiv 8 \pmod{19}$ and since order of $3$ mod $19$ is $18$ this implies that $c \equiv 3 \pmod{18}$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_50222  (c : ℕ)
  (h₀ : 0 < c)
  (h₁ : (3^c) % 19 = 8) :
  (c % 18) = 3   :=  by sorry

Source