Evaluating a polynomial at the opposite input
ProvedWorkbookSource.problem_18412lean-workbooksource-checked
If and , find .
Source: InternLM Lean-Workbook, record lean_workbook_18412 (Apache-2.0). The complete source proposition and its explicit variable declarations are preserved.
Preamble
import Mathlib open Real
Formal statement
theorem WorkbookSource.problem_18412 (f : ℝ → ℝ) (a : ℝ) (h₁ : f = fun x => x^5 + x^3 + 1) (h₂ : f a = 7) : f (-a) = -5 := by sorry
Source