mathlib3 documentation


Slash invariant forms #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

This file defines functions that are invariant under a slash_action which forms the basis for defining modular_form and cusp_form. We prove several instances for such spaces, in particular that they form a module.


slash_invariant_form_class F Γ k asserts F is a type of bundled functions that are invariant under the slash_action.

Instances of this typeclass
Instances of other typeclasses for slash_invariant_form_class
  • slash_invariant_form_class.has_sizeof_inst

Copy of a slash_invariant_form with a new to_fun equal to the old one. Useful to fix definitional equalities.

theorem slash_invariant_form.slash_action_eqn' {F : Type u_1} (k : ) (Γ : subgroup (matrix.special_linear_group (fin 2) )) [slash_invariant_form_class F Γ k] (f : F) (γ : Γ) (z : upper_half_plane) :
f z) = ((γ 1 0) * z + (γ 1 1)) ^ k * f z
@[protected, instance]