∀ {n : Type u_1} [inst : Fintype n] [inst_1 : DecidableEq n] {R : Type u_2} [inst_2 : CommRing R]
  {Γ : Subgroup (GL n R)},
  (∀ {g : GL n R}, g ∈ Γ → Matrix.GeneralLinearGroup.det g = 1 ∨ Matrix.GeneralLinearGroup.det g = -1) →
    Γ.HasDetPlusMinusOne