lean_workbook_plus_59141
ProvedGiven and , prove that .
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_59141 (ω : ℂ) (h : ω ^ 3 = 1) (h' : ω ≠ 1) : ω ^ 2 + ω + 1 = 0 := by sorry
Source
Given and , prove that .
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_59141 (ω : ℂ) (h : ω ^ 3 = 1) (h' : ω ≠ 1) : ω ^ 2 + ω + 1 = 0 := by sorry