lean_workbook_plus_71937
OpenDefine the function recursively as follows: \n\n \n\nFor all , . \n\nCompute .
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_71937 (f : ℕ → ℚ) (f_def : f 0 = 1 ∧ ∀ x, 1 ≤ x → f x = (f (x - 1) + 1) / (x + 1)) : (0! + 1! + 2! + 3! + 4! + 5! + 6! + 7!) / f 7 = 8! := by sorry
Source