lean_workbook_plus_30518
ProvedProve that if for all , then for all .
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_30518 (a : ℕ → ℕ) (h : ∀ n, a n = n) : ∀ n, a (2 * n) = a n + n := by sorry
Source
Prove that if for all , then for all .
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_30518 (a : ℕ → ℕ) (h : ∀ n, a n = n) : ∀ n, a (2 * n) = a n + n := by sorry