Documentation

Mathlib.NumberTheory.ModularForms.CongruenceSubgroups

Congruence subgroups #

This defines congruence subgroups of SL(2, ℤ) such as Γ(N), Γ₀(N) and Γ₁(N) for N a natural number.

It also contains basic results about congruence subgroups.

@[simp]

The full level N congruence subgroup of SL(2, ℤ) of matrices that reduce to the identity modulo N.

Equations
Instances For

    The full level N congruence subgroup of SL(2, ℤ) of matrices that reduce to the identity modulo N.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For

      The congruence subgroup of SL(2, ℤ) of matrices whose lower left-hand entry reduces to zero modulo N.

      Equations
      Instances For

        The group homomorphism from CongruenceSubgroup.Gamma0 to ZMod N given by mapping a matrix to its lower right-hand entry.

        Equations
        Instances For

          The congruence subgroup Gamma1 (as a subgroup of Gamma0) of matrices whose bottom row is congruent to (0, 1) modulo N.

          Equations
          Instances For
            @[simp]
            theorem CongruenceSubgroup.Gamma1_mem' {N : } {γ : (Gamma0 N)} :

            The congruence subgroup Gamma1 of SL(2, ℤ) consisting of matrices whose bottom row is congruent to (0,1) modulo N.

            Equations
            Instances For

              A congruence subgroup is a subgroup of SL(2, ℤ) which contains some Gamma N for some (N : ℕ+).

              Equations
              Instances For