lean_workbook_plus_51292

Open

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

Let $N=\prod_{k=1}^{1006}(2k-1).$ Prove that $N \equiv 3 \mod 8$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_51292 : (∏ k in Finset.Icc 1 1006, (2 * k - 1)) % 8 = 3   :=  by sorry

Source