lean_workbook_plus_78499

Open

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

What is the value of $f(0!)+f(1!)+f(2!)+f(3!)+f(4!)$ given $f(n)=n-10\\left\\lfloor\\dfrac n{10}\\right\\rfloor$ ?

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_78499 (f : ℕ → ℕ) (f_def : ∀ n, f n = n - 10 * Nat.floor (n / 10)) : f 0! + f 1! + f 2! + f 3! + f 4! = 14   :=  by sorry

Source