lean_workbook_plus_57582
ProvedSolve for all real and imaginary:
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_57582 (x : ℂ) : x^3 + 7 * x^2 + 11 * x + 5 = 0 ↔ x = -1 ∨ x = -1 ∨ x = -5 := by sorry
Source
Solve for all real and imaginary:
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_57582 (x : ℂ) : x^3 + 7 * x^2 + 11 * x + 5 = 0 ↔ x = -1 ∨ x = -1 ∨ x = -5 := by sorry