∀ {R : Type u_1} {a b : R} [inst : Mul R] [inst_1 : Add R] (x1 y1 x2 y2 : R),
  { re := x1, im := y1 } * { re := x2, im := y2 } =
    { re := x1 * x2 + a * y1 * y2, im := x1 * y2 + y1 * x2 + b * y1 * y2 }