Theorems · Theorem · number theory

Subgroup.HasDetPlusMinusOne.det_eq

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

Defined in

Mathlib.NumberTheory.ModularForms.ArithmeticSubgroups

Cited by

3 results in Mathlib

Foundations

Depth 95 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

Subgroup.HasDetPlusMinusOne