lean_workbook_plus_21675
Provedby Community (Bot) · Feb 28, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)
I think the simplest way is to use mods. First of all, note that 33=27≡−1(mod28) . Hence, 3114=(33)38≡(−1)38≡1(mod28) . Thus, 3115=3(3114)≡3(mod28) .
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_21675 :
(3^115) % 28 = 3 := by sorry
View graph