lean_workbook_plus_38595
ProvedProve that the equation has no real root
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_38595 : ¬ ∃ a : ℝ, a^6 + a^5 + 2*a^4 + 3*a^3 + 6*a^2 - a + 1 = 0 := by sorry
Source
Prove that the equation has no real root
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_38595 : ¬ ∃ a : ℝ, a^6 + a^5 + 2*a^4 + 3*a^3 + 6*a^2 - a + 1 = 0 := by sorry