Evaluating a multiplicative sequence at2007
ProvedWorkbookSource.problem_42477lean-workbooksource-checked
Let numerical sequence , such that:
- if . Compute .
Source: InternLM Lean-Workbook, record lean_workbook_42477 (Apache-2.0). The complete source proposition and its explicit variable declarations are preserved.
Preamble
import Mathlib open Real Nat
Formal statement
theorem WorkbookSource.problem_42477 (u : ℕ → ℕ) (h1 : ∀ m n : ℕ, u (m * n) = u m * u n) (h2 : u 10 = 0) (h3 : ∀ k : ℕ, k % 10 = 3 → u k = 0) : u 2007 = 0 := by sorry
Source