Theorems · Inductive type · number theory

Subgroup.HasDetPlusMinusOne

{n : Type u_1} →
  [inst : Fintype n] → [inst_1 : DecidableEq n] → {R : Type u_2} → [inst_2 : CommRing R] → Subgroup (GL n R) → Prop

Typeclass saying that a subgroup of GL(2, ℝ) has determinant contained in {±1}. Necessary so that the typeclass system can detect when the slash action is multiplicative.

Defined in

Mathlib.NumberTheory.ModularForms.ArithmeticSubgroups

Cited by

57 results in Mathlib

Foundations

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

Assumes

FintypeDecidableEqCommRing