lean_workbook_plus_61327

Proved

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

There exists a number $k$ such that $2^{p-2} + 3^{p-2} + 6^{p-2} \equiv k \pmod{p}$ with $p$ an odd prime. Find $k$ with proof.

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_61327 (p : ℕ) (hp : p.Prime) (hp1 : Odd p) : ∃ k : ℕ, (2^(p-2) + 3^(p-2) + 6^(p-2) ≡ k [ZMOD p])   :=  by sorry

Source