lean_workbook_plus_50579

Proved

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

Express $P(2)$ as $P(2)=P_1(2)+2P_2(2)=n_1+2n_2$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_50579 (P : ℕ → ℕ) (hP : ∃ P₁ P₂ : ℕ → ℕ, ∀ n, P n = P₁ n + 2 * P₂ n) : ∃ n₁ n₂ : ℕ, P 2 = n₁ + 2 * n₂   :=  by sorry

Source