lean_workbook_plus_34388

Proved

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

If $n = 74892^{359}$ x $6379^{207}$ x $9538^{179}$ x $3756^{723}$ find the remainder when n is divided by 5.

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_34388 (n : ℕ) : n = 74892^359 * 6379^207 * 9538^179 * 3756^723 → n % 5 = 4   :=  by sorry

Source