∀ {R : Type u_1} {a b : R} [inst : CommRing R] (x y : R),
  { re := x, im := y } * star { re := x, im := y } =
    (algebraMap R (QuadraticAlgebra R a b)) x * (algebraMap R (QuadraticAlgebra R a b)) x +
        (algebraMap R (QuadraticAlgebra R a b)) b * (algebraMap R (QuadraticAlgebra R a b)) x *
          (algebraMap R (QuadraticAlgebra R a b)) y -
      (algebraMap R (QuadraticAlgebra R a b)) a * (algebraMap R (QuadraticAlgebra R a b)) y *
        (algebraMap R (QuadraticAlgebra R a b)) y