lean_workbook_plus_58901

Proved

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

So we must have $3^b=1\left(\operatorname{mod}7\right)$ and thus $b=0\left(\operatorname{mod}6\right)$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_58901  (b : ℕ)
  (h₀ : b < 12)
  (h₁ : 3^b ≡ 1 [MOD 7]) :
  b ≡ 0 [MOD 6]   :=  by sorry

Source