∀ {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) (g : GL n R),
  Matrix.GeneralLinearGroup.det ((Matrix.GeneralLinearGroup.map f) g) = (Units.map ↑f) (Matrix.GeneralLinearGroup.det g)