mathlib documentation


Slash actions #

This file defines a class of slash actions, which are families of right actions of a given group parametrized by some Type. This is modeled on the slash action of GL_pos (fin 2) ℝ on the space of modular forms.

structure slash_action (β : Type u_1) (G : Type u_2) (α : Type u_3) (γ : Type u_4) [group G] [ring α] [has_smul γ α] :
Type (max u_1 u_2 u_3)

A general version of the slash action of the space of modular forms.

Instances of this typeclass
Instances of other typeclasses for slash_action
  • slash_action.has_sizeof_inst
def monoid_hom_slash_action {β : Type u_1} {G : Type u_2} {H : Type u_3} {α : Type u_4} {γ : Type u_5} [group G] [ring α] [has_smul γ α] [group H] [slash_action β G α γ] (h : H →* G) :
slash_action β H α γ

Slash_action induced by a monoid homomorphism.

noncomputable def modular_forms.slash  :

The weight k action of GL(2, ℝ)⁺ on functions f : ℍ → ℂ.