simp only [add_im, int_cast_im, mul_im, int_cast_re, MulZeroClass.zero_mul, add_zero, zero_add]
a b c : ℤω
⊢ (↑a.x + ↑a.y * { re := -1 / 2, im := rt3 / 2 }).im = ↑a.y * rt3 / 2
a b c : ℤω
⊢ ↑a.y * (rt3 / 2) = ↑a.y * rt3 / 2