lean_workbook_plus_48271
ProvedIf then .
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_48271 (f : ℝ → ℝ) (h₀ : ∀ x, f x = 28 * x^5 + 3 * x^4 - 29 * x^3 + 4 * x^2 - 7 * x + 1) : f 1 = 0 := by sorry
Source
If then .
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_48271 (f : ℝ → ℝ) (h₀ : ∀ x, f x = 28 * x^5 + 3 * x^4 - 29 * x^3 + 4 * x^2 - 7 * x + 1) : f 1 = 0 := by sorry