Structures · Algebra
Subgroup.HasDetOne
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.
- Shape
- One type argument · adds det_eq
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by0
Nothing extends this class yet.
Concrete types that are instances0
No instance on a concrete type; it is reached through other classes.
How is a type an instance?
Loading the hierarchy index…
Assumed by38
- CuspForm.toModularFormₗ
- ModularForm.IsCuspForm
- ModularForm.const
- Subgroup.HasDetOne.det_eq
- ModularForm.cuspFormSubmodule
- SlashInvariantForm.const
- SlashInvariantForm.slash_action_eqn'
- ModularForm.isCuspForm_iff
- ModularForm.CuspForm.equivCuspFormSubmodule
- ModularForm.eq_zero_of_neg_one_mem
- SlashInvariantForm.slash_action_eqn''
- ModularForm.mem_cuspFormSubmodule_iff
- SlashInvariantForm.instIsSMulApplyUpperHalfPlaneComplex
- SlashInvariantForm.const.congr_simp
- ModularForm.IsCuspForm.congr_simp
- CuspForm.toModularFormₗ_apply
- Subgroup.instHasDetOneMinGeneralLinearGroup
- ModularForm.instGAlgebra
- ModularForm.instModuleComplexOfHasDetOneFinOfNatNatReal
- SlashInvariantFormClass.petersson_smul
- ModularForm.coe_const
- Subgroup.instHasDetOneMinGeneralLinearGroup_1
- CuspForm.IsGLPos.instSMulApply
- Subgroup.instHasDetPlusMinusOneOfHasDetOne
- CuspForm.toModularFormₗ_eq_coe
- SlashInvariantForm.instModuleComplex
- ModularForm.const_apply
- ModularForm.const.congr_simp
- instHasDetOneAdjoinNegOneOfFactEvenNatCard
- ModularForm.CuspForm.isCuspForm_toModularFormₗ
- ModularForm.instIsSMulApplyℂ
- CuspForm.IsGLPos.instSMul
- CuspForm.instModuleComplexOfHasDetOneFinOfNatNatReal
- ModularForm.instSMulℂ
- SlashInvariantForm.instSMul
- CuspForm.toModularFormₗ_injective
- Subgroup.instHasDetOneHSMulConjActGeneralLinearGroup
- SlashInvariantForm.coe_const
Ancestors0
No ancestors.