lean_workbook_plus_72704
ProvedShow that the equation doesn't have any real solution.
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_72704 : ¬ ∃ x : ℝ, x^4 + x^3 - x + 1 = 0 := by sorry
Source
Show that the equation doesn't have any real solution.
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_72704 : ¬ ∃ x : ℝ, x^4 + x^3 - x + 1 = 0 := by sorry