simp only [complexω]
case a
a b c : ℤω
⊢ complexω.re * complexω.re - complexω.im * complexω.im = (-complexω - 1).re
case a
a b c : ℤω
⊢ -1 / 2 * (-1 / 2) - rt3 / 2 * (rt3 / 2) = (-{ re := -1 / 2, im := rt3 / 2 } - 1).re