Theorems · Inductive type · number theory

Subgroup.HasDetOne

{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(n, R) is contained in SL(n, R). Necessary so that the typeclass system can detect when the slash action is ℂ-linear.

Defined in

Mathlib.NumberTheory.ModularForms.ArithmeticSubgroups

Cited by

18 results in Mathlib

Foundations

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

Assumes

FintypeDecidableEqCommRing