Structures · Algebra
SlashInvariantFormClass
SlashInvariantFormClass F Γ k asserts F is a type of bundled functions that are invariant
under the SlashAction.
- Shape
- 3 explicit arguments · adds slash_action_eq
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by2
Concrete types that are instances1
- SlashInvariantForm
How is a type an instance?
Loading the hierarchy index…
Assumed by24
- SlashInvariantFormClass.periodic_comp_ofComplex
- SlashInvariantForm.quotientFunc
- SlashInvariantForm.slash_action_eqn
- SlashInvariantFormClass.slash_action_eq
- SlashInvariantForm.norm
- SlashInvariantForm.slash_action_eqn_SL''
- SlashInvariantForm.vAdd_apply_of_mem_strictPeriods
- SlashInvariantForm.slash_action_eqn'
- SlashInvariantFormClass.norm_petersson_smul
- SlashInvariantFormClass.eq_cuspFunction
- SlashInvariantForm.translate
- SlashInvariantForm.slash_action_eqn''
- SlashInvariantForm.trace
- SlashInvariantForm.wt_eq_zero_of_eq_const
- SlashInvariantForm.norm.congr_simp
- SlashInvariantForm.quotientFunc_smul
- SlashInvariantForm.quotientFunc_mk
- SlashInvariantFormClass.petersson_smul
- SlashInvariantForm.exists_one_half_le_im_and_norm_le
- SlashInvariantForm.coe_trace
- SlashInvariantForm.instCoeTCOfSlashInvariantFormClass
- SlashInvariantForm.coe_norm
- SlashInvariantForm.quotientFunc.congr_simp
- SlashInvariantForm.coe_translate
Ancestors0
No ancestors.