∀ {R : Type u_1} [inst : CommRing R] {M : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  {Q : QuadraticForm R M} (_x _y : ↥(pinGroup Q)),
  { val := ↑(_x * _y), inv := ↑(_x * _y)⁻¹, val_inv := ⋯, inv_val := ⋯ } =
    { val := ↑_x, inv := ↑_x⁻¹, val_inv := ⋯, inv_val := ⋯ } * { val := ↑_y, inv := ↑_y⁻¹, val_inv := ⋯, inv_val := ⋯ }