Lean-Workbook Plus 72890: Fifteen factorial is divisible by one thousand

Proved

WorkbookRestored.plus_72890

by wamlart · Sep 12, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

lean-workbookrestored-importssource-checked

$15!\equiv0\pmod{1000}$ .

Source: Lean-Workbook row lean_workbook_plus_72890 (Apache-2.0), original record. This repair only restores required imports and namespaces; the mathematical declaration is unchanged.

Preamble

import Mathlib.Data.Nat.Factorial.Basic
open Nat

Formal statement

theorem WorkbookRestored.plus_72890 : 15! % 1000 = 0   :=  by sorry

Source

https://huggingface.co/datasets/internlm/Lean-Workbook/blob/main/lean_workbook.json, row lean_workbook_plus_72890; immutable original Prove2Me node 9a2d6cba-e7fa-4c1b-888b-12ba07253159

View graph