lean_workbook_plus_19433
ProvedExpress in terms of where .
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_19433 (a b : ℕ → ℕ) (h₁ : ∀ n, a n = 2 * b n) : a = fun n ↦ 2 * b n := by sorry
Source
Express in terms of where .
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_19433 (a b : ℕ → ℕ) (h₁ : ∀ n, a n = 2 * b n) : a = fun n ↦ 2 * b n := by sorry