lean_workbook_plus_61807
ProvedLet be a linear function, . Then, if this works out, our answer will be just , because the remainder when a linear function is divided by a quadratic is just . Now, using synthetic division, the remainder when is divided by is . Similarly, for , the remainder is . Solving, we get and , so the function is Success! Our answer is .
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_61807 (a b : ℝ) (f : ℝ → ℝ) (h₀ : ∀ x, f x = a * x + b) (h₁ : f 2 = 3) (h₂ : f 3 = 2) : a^2 + b^2 = 26 := by sorry
Source