Prove2Me

lean_workbook_plus_24451

Proved

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

Is a linear function: f(x)=axf(x)=ax . 2008a=3012  ⟹  a=301220082008a=3012\implies a=\frac{3012}{2008} . f(2009)=3012⋅20092008f(2009)=\frac{3012\cdot 2009}{2008}

Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_24451  (a : ℝ)
  (f : ℝ → ℝ)
  (h₀ : ∀ x, f x = a * x)
  (h₁ : 2008 * a = 3012) :
  f 2009 = 3012 * 2009 / 2008   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook

View graph