Structures · Algebra
Subgroup.HasDetPlusMinusOne
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.
- 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 instances1
- Fin
How is a type an instance?
Loading the hierarchy index…
Assumed by79
- ModularForm.mul
- ModularForm.pow
- Subgroup.strictWidthInfty_pos_iff
- ModularForm.norm
- ModularForm.qExpansion_mul
- ModularForm.qExpansionRingHom
- ModularForm.coe_mul
- Subgroup.HasDetPlusMinusOne.det_eq
- SlashInvariantForm.constℝ
- UpperHalfPlane.IsZeroAtImInfty.petersson_exp_decay_left
- SlashInvariantForm.mul
- SlashInvariantForm.norm
- ModularFormClass.exp_decay_atImInfty'
- SlashInvariantForm.prod
- Subgroup.HasDetPlusMinusOne.abs_det
- SlashInvariantFormClass.norm_petersson_smul
- ModularForm.constℝ
- ModularForm.coe_norm
- UpperHalfPlane.IsZeroAtImInfty.petersson_exp_decay_right
- ModularForm.qExpansionRingHom_apply
- ModularForm.coe_pow
- UpperHalfPlane.IsZeroAtImInfty.petersson_isZeroAtImInfty_left
- ModularForm.isZeroAtImInfty_of_valueAtInfty_eq_zero
- ModularForm.qExpansion_one
- CuspForm.mulModularForm
- ModularForm.prod
- ModularForm.prodEqualWeights
- Subgroup.HasDetPlusMinusOne.isParabolic_iff_of_upperTriangular
- ModularForm.norm_ne_zero
- ModularForm.directSum_of_pow
- ModularFormClass.exp_decay_sub_atImInfty'
- SlashInvariantForm.prodEqualWeights
- SlashInvariantForm.prod.congr_simp
- ModularForm.instGMulIntOfHasDetPlusMinusOneFinOfNatNatReal
- SlashInvariantForm.instNatCastOfNatIntOfHasDetPlusMinusOneFinNatReal
- Subgroup.instHasDetPlusMinusOneHSMulConjActGeneralLinearGroup
- CuspFormClass.exp_decay_atImInfty'
- ModularForm.mul_ne_zero
- ModularForm.constℝ_apply
- SlashInvariantForm.coe_intCast
- SlashInvariantForm.norm.congr_simp
- ModularForm.norm_eq_zero_iff
- ModularForm.gnpow_eq_pow
- ModularForm.coe_natCast
- ModularForm.one_coe_eq_one
- ModularForm.mul.congr_simp
- ModularForm.norm.congr_simp
- ModularForm.instOneOfNatIntOfHasDetPlusMinusOneFinNatReal
- SlashInvariantForm.coe_prod
- ModularForm.toSlashInvariantForm_natCast
Ancestors0
No ancestors.