∀ {n : Type u} [inst : DecidableEq n] [inst_1 : Fintype n] {R : Type v} [inst_2 : CommRing R] {S : Type u_1}
  [inst_3 : CommRing S] (f : R →+* S) (i j : n) (g : GL n R), ↑((Matrix.GeneralLinearGroup.map f) g) i j = f (↑g i j)