∀ {n : Type u_1} {R : Type u₂} [inst : DecidableEq n] [inst_1 : CommRing R] (i j : n) [inst_2 : Fintype n] (a : n)
  (c : R) (M : Matrix n n R), (M * Matrix.transvection i j c) a j = M a j + c * M a i