lean_workbook_plus_18646

Proved

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

Show that $1981 \mid 145^{1981} + 3114\cdot 138^{1981}$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_18646 : 1981 ∣ 145 ^ 1981 + 3114 * 138 ^ 1981   :=  by sorry

Source