lean_workbook_plus_24600

Proved

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

We see $7^4=2401 \equiv 1 \pmod{100}$ . So $(7^4)^{502} \equiv 1 \pmod{100} \rightarrow (7^4)^{502}.7^2 \equiv 49 \pmod{100}$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_24600 :
  (7^4)^502 * 7^2 ≡ 49 [MOD 100]   :=  by sorry

Source