∀ {n : Type u_1} [inst : Fintype n] [inst_1 : DecidableEq n] {R : Type u_2} [inst_2 : CommRing R] {S : Type u_3}
  [inst_3 : CommRing S] [inst_4 : Algebra R S] (Γ : Subgroup (Matrix.SpecialLinearGroup n R)),
  (Subgroup.map (Matrix.SpecialLinearGroup.mapGL S) Γ).HasDetOne