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