∀ {R : Type u_1} [inst : CommRing R] (c : R) (m n : Fin 3 → R),
  ![m 1 * (c • n) 2 - m 2 * (c • n) 1, m 2 * (c • n) 0 - m 0 * (c • n) 2, m 0 * (c • n) 1 - m 1 * (c • n) 0] =
    c • ![m 1 * n 2 - m 2 * n 1, m 2 * n 0 - m 0 * n 2, m 0 * n 1 - m 1 * n 0]