AutomorphicForm.GLn.IsSlowlyIncreasing.mk
  {nℕ : ℕNat : TypeThe natural numbers, starting at zero.

This type is special-cased by both the kernel and the compiler, and overridden with an efficient
implementation. Both use a fast arbitrary-precision arithmetic library (usually
[GMP](https://gmplib.org/)); at runtime, `Nat` values that are sufficiently small are unboxed.
} {fGL (Fin n) ℝ → ℂ : GLMatrix.GeneralLinearGroup.{u, v} (n : Type u) (R : Type v) [DecidableEq n] [Fintype n] [Semiring R] : Type (max v u)`GL n R` is the group of `n` by `n` `R`-matrices with unit determinant.
Defined as a subtype of matrices  (FinFin (n : ℕ) : TypeNatural numbers less than some upper bound.

In particular, a `Fin n` is a natural number `i` with the constraint that `i < n`. It is the
canonical type with `n` elements.
 nℕ) ℝReal : TypeThe type `ℝ` of real numbers constructed as equivalence classes of Cauchy sequences of rational
numbers.  → ℂComplex : TypeComplex numbers consist of two `Real`s: a real part `re` and an imaginary part `im`. }
  (bounded_by∃ C N, ∀ (M : GL (Fin n) ℝ), ‖f M‖ ≤ C * AutomorphicForm.GLn.s ↑M ^ N :
    ∃ Cℝ Nℕ,
      ∀ (MGL (Fin n) ℝ : GLMatrix.GeneralLinearGroup.{u, v} (n : Type u) (R : Type v) [DecidableEq n] [Fintype n] [Semiring R] : Type (max v u)`GL n R` is the group of `n` by `n` `R`-matrices with unit determinant.
Defined as a subtype of matrices  (FinFin (n : ℕ) : TypeNatural numbers less than some upper bound.

In particular, a `Fin n` is a natural number `i` with the constraint that `i < n`. It is the
canonical type with `n` elements.
 nℕ) ℝReal : TypeThe type `ℝ` of real numbers constructed as equivalence classes of Cauchy sequences of rational
numbers. ),
        ‖Norm.norm.{u_8} {E : Type u_8} [self : Norm E] : E → ℝthe `ℝ`-valued norm function. fGL (Fin n) ℝ → ℂ MGL (Fin n) ℝ‖Norm.norm.{u_8} {E : Type u_8} [self : Norm E] : E → ℝthe `ℝ`-valued norm function.  ≤LE.le.{u} {α : Type u} [self : LE α] : α → α → PropThe less-equal relation: `x ≤ y` 

Conventions for notations in identifiers:

 * The recommended spelling of `≤` in identifiers is `le`.

 * The recommended spelling of `<=` in identifiers is `le` (prefer `≤` over `<=`).
          Cℝ *HMul.hMul.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HMul α β γ] : α → β → γ`a * b` computes the product of `a` and `b`.
The meaning of this notation is type-dependent. 

Conventions for notations in identifiers:

 * The recommended spelling of `*` in identifiers is `mul`.
            AutomorphicForm.GLn.sAutomorphicForm.GLn.s {n : ℕ} (M : Matrix (Fin n) (Fin n) ℝ) : ℝ ↑MGL (Fin n) ℝ ^HPow.hPow.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HPow α β γ] : α → β → γ`a ^ b` computes `a` to the power of `b`.
The meaning of this notation is type-dependent. 

Conventions for notations in identifiers:

 * The recommended spelling of `^` in identifiers is `pow`.
              Nℕ) :
  AutomorphicForm.GLn.IsSlowlyIncreasingAutomorphicForm.GLn.IsSlowlyIncreasing {n : ℕ} (f : GL (Fin n) ℝ → ℂ) : Prop
    fGL (Fin n) ℝ → ℂ

AutomorphicForm.GLn.Weight.mk {nℕ : ℕNat : TypeThe natural numbers, starting at zero.

This type is special-cased by both the kernel and the compiler, and overridden with an efficient
implementation. Both use a fast arbitrary-precision arithmetic library (usually
[GMP](https://gmplib.org/)); at runtime, `Nat` values that are sufficiently small are unboxed.
}
  (wAutomorphicForm.GLn.preweight n : AutomorphicForm.GLn.preweightAutomorphicForm.GLn.preweight (n : ℕ) : Type nℕ)
  (isSimpleCategoryTheory.Simple (AutomorphicForm.GLn.preweight.fdRep n w) :
    CategoryTheory.SimpleCategoryTheory.Simple.{v, u} {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C]
  (X : C) : PropAn object is simple if monomorphisms into it are (exclusively) either isomorphisms or zero. 
      (AutomorphicForm.GLn.preweight.fdRepAutomorphicForm.GLn.preweight.fdRep (n : ℕ) (w : AutomorphicForm.GLn.preweight n) :
  FDRep ℂ ↥(Matrix.orthogonalGroup (Fin n) ℝ)
        nℕ wAutomorphicForm.GLn.preweight n)) :
  AutomorphicForm.GLn.WeightAutomorphicForm.GLn.Weight (n : ℕ) : Type nℕ

AutomorphicForm.GLn.AutomorphicFormForGLnOverQ.mk
  {nℕ : ℕNat : TypeThe natural numbers, starting at zero.

This type is special-cased by both the kernel and the compiler, and overridden with an efficient
implementation. Both use a fast arbitrary-precision arithmetic library (usually
[GMP](https://gmplib.org/)); at runtime, `Nat` values that are sufficiently small are unboxed.
}
  {ρAutomorphicForm.GLn.Weight n : AutomorphicForm.GLn.WeightAutomorphicForm.GLn.Weight (n : ℕ) : Type nℕ}
  (toFunGL (Fin n) (IsDedekindDomain.FiniteAdeleRing ℤ ℚ) × GL (Fin n) ℝ → ℂ :
    GLMatrix.GeneralLinearGroup.{u, v} (n : Type u) (R : Type v) [DecidableEq n] [Fintype n] [Semiring R] : Type (max v u)`GL n R` is the group of `n` by `n` `R`-matrices with unit determinant.
Defined as a subtype of matrices  (FinFin (n : ℕ) : TypeNatural numbers less than some upper bound.

In particular, a `Fin n` is a natural number `i` with the constraint that `i < n`. It is the
canonical type with `n` elements.
 nℕ)
          (IsDedekindDomain.FiniteAdeleRingIsDedekindDomain.FiniteAdeleRing.{u_1, u_2} (R : Type u_1) [CommRing R] [IsDedekindDomain R] (K : Type u_2) [Field K]
  [Algebra R K] [IsFractionRing R K] : Type (max u_2 u_1)If `K` is the field of fractions of the Dedekind domain `R` then `FiniteAdeleRing R K` is
the ring of finite adeles of `K`, defined as the restricted product of the completions
`K_v` with respect to the subrings `R_v`. Here `v` runs through the nonzero primes of `R`
and the restricted product is the subring of `∏_v K_v` consisting of elements which
are in `R_v` for all but finitely many `v`.

            ℤInt : TypeThe integers.

This type is special-cased by the compiler and overridden with an efficient implementation. The
runtime has a special representation for `Int` that stores “small” signed numbers directly, while
larger numbers use a fast arbitrary-precision arithmetic library (usually
[GMP](https://gmplib.org/)). A “small number” is an integer that can be encoded with one fewer bits
than the platform's pointer size (i.e. 63 bits on 64-bit architectures and 31 bits on 32-bit
architectures).
 ℚRat : TypeRational numbers, implemented as a pair of integers `num / den` such that the
denominator is positive and the numerator and denominator are coprime.
) ×Prod.{u, v} (α : Type u) (β : Type v) : Type (max u v)The product type, usually written `α × β`. Product types are also called pair or tuple types.
Elements of this type are pairs in which the first element is an `α` and the second element is a
`β`.

Products nest to the right, so `(x, y, z) : α × β × γ` is equivalent to `(x, (y, z)) : α × (β × γ)`.


Conventions for notations in identifiers:

 * The recommended spelling of `×` in identifiers is `Prod`.
        GLMatrix.GeneralLinearGroup.{u, v} (n : Type u) (R : Type v) [DecidableEq n] [Fintype n] [Semiring R] : Type (max v u)`GL n R` is the group of `n` by `n` `R`-matrices with unit determinant.
Defined as a subtype of matrices  (FinFin (n : ℕ) : TypeNatural numbers less than some upper bound.

In particular, a `Fin n` is a natural number `i` with the constraint that `i < n`. It is the
canonical type with `n` elements.
 nℕ) ℝReal : TypeThe type `ℝ` of real numbers constructed as equivalence classes of Cauchy sequences of rational
numbers.  →
      ℂComplex : TypeComplex numbers consist of two `Real`s: a real part `re` and an imaginary part `im`. )
  (is_smoothAutomorphicForm.GLn.IsSmooth toFun :
    AutomorphicForm.GLn.IsSmoothAutomorphicForm.GLn.IsSmooth {n : ℕ} (f : GL (Fin n) (IsDedekindDomain.FiniteAdeleRing ℤ ℚ) × GL (Fin n) ℝ → ℂ) : Prop toFunGL (Fin n) (IsDedekindDomain.FiniteAdeleRing ℤ ℚ) × GL (Fin n) ℝ → ℂ)
  (is_periodic∀ (g : GL (Fin n) ℚ) (x : GL (Fin n) (IsDedekindDomain.FiniteAdeleRing ℤ ℚ)) (y : GL (Fin n) ℝ),
  toFun
      (((algebraMap ℚ (IsDedekindDomain.FiniteAdeleRing ℤ ℚ)).GL (Fin n)) g * x, ((algebraMap ℚ ℝ).GL (Fin n)) g * y) =
    toFun (x, y) :
    ∀ (gGL (Fin n) ℚ : GLMatrix.GeneralLinearGroup.{u, v} (n : Type u) (R : Type v) [DecidableEq n] [Fintype n] [Semiring R] : Type (max v u)`GL n R` is the group of `n` by `n` `R`-matrices with unit determinant.
Defined as a subtype of matrices  (FinFin (n : ℕ) : TypeNatural numbers less than some upper bound.

In particular, a `Fin n` is a natural number `i` with the constraint that `i < n`. It is the
canonical type with `n` elements.
 nℕ) ℚRat : TypeRational numbers, implemented as a pair of integers `num / den` such that the
denominator is positive and the numerator and denominator are coprime.
)
      (xGL (Fin n) (IsDedekindDomain.FiniteAdeleRing ℤ ℚ) :
        GLMatrix.GeneralLinearGroup.{u, v} (n : Type u) (R : Type v) [DecidableEq n] [Fintype n] [Semiring R] : Type (max v u)`GL n R` is the group of `n` by `n` `R`-matrices with unit determinant.
Defined as a subtype of matrices  (FinFin (n : ℕ) : TypeNatural numbers less than some upper bound.

In particular, a `Fin n` is a natural number `i` with the constraint that `i < n`. It is the
canonical type with `n` elements.
 nℕ)
          (IsDedekindDomain.FiniteAdeleRingIsDedekindDomain.FiniteAdeleRing.{u_1, u_2} (R : Type u_1) [CommRing R] [IsDedekindDomain R] (K : Type u_2) [Field K]
  [Algebra R K] [IsFractionRing R K] : Type (max u_2 u_1)If `K` is the field of fractions of the Dedekind domain `R` then `FiniteAdeleRing R K` is
the ring of finite adeles of `K`, defined as the restricted product of the completions
`K_v` with respect to the subrings `R_v`. Here `v` runs through the nonzero primes of `R`
and the restricted product is the subring of `∏_v K_v` consisting of elements which
are in `R_v` for all but finitely many `v`.

            ℤInt : TypeThe integers.

This type is special-cased by the compiler and overridden with an efficient implementation. The
runtime has a special representation for `Int` that stores “small” signed numbers directly, while
larger numbers use a fast arbitrary-precision arithmetic library (usually
[GMP](https://gmplib.org/)). A “small number” is an integer that can be encoded with one fewer bits
than the platform's pointer size (i.e. 63 bits on 64-bit architectures and 31 bits on 32-bit
architectures).
 ℚRat : TypeRational numbers, implemented as a pair of integers `num / den` such that the
denominator is positive and the numerator and denominator are coprime.
))
      (yGL (Fin n) ℝ : GLMatrix.GeneralLinearGroup.{u, v} (n : Type u) (R : Type v) [DecidableEq n] [Fintype n] [Semiring R] : Type (max v u)`GL n R` is the group of `n` by `n` `R`-matrices with unit determinant.
Defined as a subtype of matrices  (FinFin (n : ℕ) : TypeNatural numbers less than some upper bound.

In particular, a `Fin n` is a natural number `i` with the constraint that `i < n`. It is the
canonical type with `n` elements.
 nℕ) ℝReal : TypeThe type `ℝ` of real numbers constructed as equivalence classes of Cauchy sequences of rational
numbers. ),
      toFunGL (Fin n) (IsDedekindDomain.FiniteAdeleRing ℤ ℚ) × GL (Fin n) ℝ → ℂ
          (Prod.mk.{u, v} {α : Type u} {β : Type v} (fst : α) (snd : β) : α × βConstructs a pair. This is usually written `(x, y)` instead of `Prod.mk x y`.


Conventions for notations in identifiers:

 * The recommended spelling of `(a, b)` in identifiers is `mk`.((algebraMapalgebraMap.{u, v} (R : Type u) (A : Type v) [CommSemiring R] [Semiring A] [Algebra R A] : R →+* AEmbedding `R →+* A` given by `Algebra` structure.  ℚRat : TypeRational numbers, implemented as a pair of integers `num / den` such that the
denominator is positive and the numerator and denominator are coprime.

                      (IsDedekindDomain.FiniteAdeleRingIsDedekindDomain.FiniteAdeleRing.{u_1, u_2} (R : Type u_1) [CommRing R] [IsDedekindDomain R] (K : Type u_2) [Field K]
  [Algebra R K] [IsFractionRing R K] : Type (max u_2 u_1)If `K` is the field of fractions of the Dedekind domain `R` then `FiniteAdeleRing R K` is
the ring of finite adeles of `K`, defined as the restricted product of the completions
`K_v` with respect to the subrings `R_v`. Here `v` runs through the nonzero primes of `R`
and the restricted product is the subring of `∏_v K_v` consisting of elements which
are in `R_v` for all but finitely many `v`.

                        ℤInt : TypeThe integers.

This type is special-cased by the compiler and overridden with an efficient implementation. The
runtime has a special representation for `Int` that stores “small” signed numbers directly, while
larger numbers use a fast arbitrary-precision arithmetic library (usually
[GMP](https://gmplib.org/)). A “small number” is an integer that can be encoded with one fewer bits
than the platform's pointer size (i.e. 63 bits on 64-bit architectures and 31 bits on 32-bit
architectures).
 ℚRat : TypeRational numbers, implemented as a pair of integers `num / den` such that the
denominator is positive and the numerator and denominator are coprime.
)).GLRingHom.GL.{u_1, u_2, u_3} {A : Type u_1} {B : Type u_2} [CommRing A] [CommRing B] (φ : A →+* B) (m : Type u_3)
  [Fintype m] [DecidableEq m] : GL m A →* GL m B
                  (FinFin (n : ℕ) : TypeNatural numbers less than some upper bound.

In particular, a `Fin n` is a natural number `i` with the constraint that `i < n`. It is the
canonical type with `n` elements.
 nℕ))
                gGL (Fin n) ℚ *HMul.hMul.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HMul α β γ] : α → β → γ`a * b` computes the product of `a` and `b`.
The meaning of this notation is type-dependent. 

Conventions for notations in identifiers:

 * The recommended spelling of `*` in identifiers is `mul`.
              xGL (Fin n) (IsDedekindDomain.FiniteAdeleRing ℤ ℚ),Prod.mk.{u, v} {α : Type u} {β : Type v} (fst : α) (snd : β) : α × βConstructs a pair. This is usually written `(x, y)` instead of `Prod.mk x y`.


Conventions for notations in identifiers:

 * The recommended spelling of `(a, b)` in identifiers is `mk`.
            ((algebraMapalgebraMap.{u, v} (R : Type u) (A : Type v) [CommSemiring R] [Semiring A] [Algebra R A] : R →+* AEmbedding `R →+* A` given by `Algebra` structure.  ℚRat : TypeRational numbers, implemented as a pair of integers `num / den` such that the
denominator is positive and the numerator and denominator are coprime.
 ℝReal : TypeThe type `ℝ` of real numbers constructed as equivalence classes of Cauchy sequences of rational
numbers. ).GLRingHom.GL.{u_1, u_2, u_3} {A : Type u_1} {B : Type u_2} [CommRing A] [CommRing B] (φ : A →+* B) (m : Type u_3)
  [Fintype m] [DecidableEq m] : GL m A →* GL m B
                  (FinFin (n : ℕ) : TypeNatural numbers less than some upper bound.

In particular, a `Fin n` is a natural number `i` with the constraint that `i < n`. It is the
canonical type with `n` elements.
 nℕ))
                gGL (Fin n) ℚ *HMul.hMul.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HMul α β γ] : α → β → γ`a * b` computes the product of `a` and `b`.
The meaning of this notation is type-dependent. 

Conventions for notations in identifiers:

 * The recommended spelling of `*` in identifiers is `mul`.
              yGL (Fin n) ℝ)Prod.mk.{u, v} {α : Type u} {β : Type v} (fst : α) (snd : β) : α × βConstructs a pair. This is usually written `(x, y)` instead of `Prod.mk x y`.


Conventions for notations in identifiers:

 * The recommended spelling of `(a, b)` in identifiers is `mk`. =Eq.{u_1} {α : Sort u_1} : α → α → PropThe equality relation. It has one introduction rule, `Eq.refl`.
We use `a = b` as notation for `Eq a b`.
A fundamental property of equality is that it is an equivalence relation.
```
variable (α : Type) (a b c d : α)
variable (hab : a = b) (hcb : c = b) (hcd : c = d)

example : a = d :=
  Eq.trans (Eq.trans hab (Eq.symm hcb)) hcd
```
Equality is much more than an equivalence relation, however. It has the important property that every assertion
respects the equivalence, in the sense that we can substitute equal expressions without changing the truth value.
That is, given `h1 : a = b` and `h2 : p a`, we can construct a proof for `p b` using substitution: `Eq.subst h1 h2`.
Example:
```
example (α : Type) (a b : α) (p : α → Prop)
        (h1 : a = b) (h2 : p a) : p b :=
  Eq.subst h1 h2

example (α : Type) (a b : α) (p : α → Prop)
    (h1 : a = b) (h2 : p a) : p b :=
  h1 ▸ h2
```
The triangle in the second presentation is a macro built on top of `Eq.subst` and `Eq.symm`, and you can enter it by typing `\t`.
For more information: [Equality](https://lean-lang.org/theorem_proving_in_lean4/quantifiers_and_equality.html#equality)


Conventions for notations in identifiers:

 * The recommended spelling of `=` in identifiers is `eq`.
        toFunGL (Fin n) (IsDedekindDomain.FiniteAdeleRing ℤ ℚ) × GL (Fin n) ℝ → ℂ (Prod.mk.{u, v} {α : Type u} {β : Type v} (fst : α) (snd : β) : α × βConstructs a pair. This is usually written `(x, y)` instead of `Prod.mk x y`.


Conventions for notations in identifiers:

 * The recommended spelling of `(a, b)` in identifiers is `mk`.xGL (Fin n) (IsDedekindDomain.FiniteAdeleRing ℤ ℚ),Prod.mk.{u, v} {α : Type u} {β : Type v} (fst : α) (snd : β) : α × βConstructs a pair. This is usually written `(x, y)` instead of `Prod.mk x y`.


Conventions for notations in identifiers:

 * The recommended spelling of `(a, b)` in identifiers is `mk`. yGL (Fin n) ℝ)Prod.mk.{u, v} {α : Type u} {β : Type v} (fst : α) (snd : β) : α × βConstructs a pair. This is usually written `(x, y)` instead of `Prod.mk x y`.


Conventions for notations in identifiers:

 * The recommended spelling of `(a, b)` in identifiers is `mk`.)
  (is_slowly_increasing∀ (x : GL (Fin n) (IsDedekindDomain.FiniteAdeleRing ℤ ℚ)), AutomorphicForm.GLn.IsSlowlyIncreasing fun y ↦ toFun (x, y) :
    ∀
      (xGL (Fin n) (IsDedekindDomain.FiniteAdeleRing ℤ ℚ) :
        GLMatrix.GeneralLinearGroup.{u, v} (n : Type u) (R : Type v) [DecidableEq n] [Fintype n] [Semiring R] : Type (max v u)`GL n R` is the group of `n` by `n` `R`-matrices with unit determinant.
Defined as a subtype of matrices  (FinFin (n : ℕ) : TypeNatural numbers less than some upper bound.

In particular, a `Fin n` is a natural number `i` with the constraint that `i < n`. It is the
canonical type with `n` elements.
 nℕ)
          (IsDedekindDomain.FiniteAdeleRingIsDedekindDomain.FiniteAdeleRing.{u_1, u_2} (R : Type u_1) [CommRing R] [IsDedekindDomain R] (K : Type u_2) [Field K]
  [Algebra R K] [IsFractionRing R K] : Type (max u_2 u_1)If `K` is the field of fractions of the Dedekind domain `R` then `FiniteAdeleRing R K` is
the ring of finite adeles of `K`, defined as the restricted product of the completions
`K_v` with respect to the subrings `R_v`. Here `v` runs through the nonzero primes of `R`
and the restricted product is the subring of `∏_v K_v` consisting of elements which
are in `R_v` for all but finitely many `v`.

            ℤInt : TypeThe integers.

This type is special-cased by the compiler and overridden with an efficient implementation. The
runtime has a special representation for `Int` that stores “small” signed numbers directly, while
larger numbers use a fast arbitrary-precision arithmetic library (usually
[GMP](https://gmplib.org/)). A “small number” is an integer that can be encoded with one fewer bits
than the platform's pointer size (i.e. 63 bits on 64-bit architectures and 31 bits on 32-bit
architectures).
 ℚRat : TypeRational numbers, implemented as a pair of integers `num / den` such that the
denominator is positive and the numerator and denominator are coprime.
)),
      AutomorphicForm.GLn.IsSlowlyIncreasingAutomorphicForm.GLn.IsSlowlyIncreasing {n : ℕ} (f : GL (Fin n) ℝ → ℂ) : Prop
        fun yGL (Fin n) ℝ ↦ toFunGL (Fin n) (IsDedekindDomain.FiniteAdeleRing ℤ ℚ) × GL (Fin n) ℝ → ℂ (Prod.mk.{u, v} {α : Type u} {β : Type v} (fst : α) (snd : β) : α × βConstructs a pair. This is usually written `(x, y)` instead of `Prod.mk x y`.


Conventions for notations in identifiers:

 * The recommended spelling of `(a, b)` in identifiers is `mk`.xGL (Fin n) (IsDedekindDomain.FiniteAdeleRing ℤ ℚ),Prod.mk.{u, v} {α : Type u} {β : Type v} (fst : α) (snd : β) : α × βConstructs a pair. This is usually written `(x, y)` instead of `Prod.mk x y`.


Conventions for notations in identifiers:

 * The recommended spelling of `(a, b)` in identifiers is `mk`. yGL (Fin n) ℝ)Prod.mk.{u, v} {α : Type u} {β : Type v} (fst : α) (snd : β) : α × βConstructs a pair. This is usually written `(x, y)` instead of `Prod.mk x y`.


Conventions for notations in identifiers:

 * The recommended spelling of `(a, b)` in identifiers is `mk`.)
  (has_finite_level∃ U, AutomorphicForm.GLn.IsConstantOn U toFun :
    ∃ USubgroup (GL (Fin n) (IsDedekindDomain.FiniteAdeleRing ℤ ℚ)),
      AutomorphicForm.GLn.IsConstantOnAutomorphicForm.GLn.IsConstantOn {n : ℕ} (U : Subgroup (GL (Fin n) (IsDedekindDomain.FiniteAdeleRing ℤ ℚ)))
  (f : GL (Fin n) (IsDedekindDomain.FiniteAdeleRing ℤ ℚ) × GL (Fin n) ℝ → ℂ) : Prop USubgroup (GL (Fin n) (IsDedekindDomain.FiniteAdeleRing ℤ ℚ))
        toFunGL (Fin n) (IsDedekindDomain.FiniteAdeleRing ℤ ℚ) × GL (Fin n) ℝ → ℂ)
  (is_finite_cod∀ (x : GL (Fin n) (IsDedekindDomain.FiniteAdeleRing ℤ ℚ)),
  FiniteDimensional ℂ
    (↥(AutomorphicForm.GLn.Z (GL (Fin n) ℝ) (Matrix (Fin n) (Fin n) ℝ)) ⧸
      Submodule.comap (AutomorphicForm.GLn.actionTensorCAlg'3 (GL (Fin n) ℝ) (Matrix (Fin n) (Fin n) ℝ)).toLinearMap
        (AutomorphicForm.GLn.annihilator ⟨fun y ↦ toFun (x, y), ⋯⟩)) :
    ∀
      (xGL (Fin n) (IsDedekindDomain.FiniteAdeleRing ℤ ℚ) :
        GLMatrix.GeneralLinearGroup.{u, v} (n : Type u) (R : Type v) [DecidableEq n] [Fintype n] [Semiring R] : Type (max v u)`GL n R` is the group of `n` by `n` `R`-matrices with unit determinant.
Defined as a subtype of matrices  (FinFin (n : ℕ) : TypeNatural numbers less than some upper bound.

In particular, a `Fin n` is a natural number `i` with the constraint that `i < n`. It is the
canonical type with `n` elements.
 nℕ)
          (IsDedekindDomain.FiniteAdeleRingIsDedekindDomain.FiniteAdeleRing.{u_1, u_2} (R : Type u_1) [CommRing R] [IsDedekindDomain R] (K : Type u_2) [Field K]
  [Algebra R K] [IsFractionRing R K] : Type (max u_2 u_1)If `K` is the field of fractions of the Dedekind domain `R` then `FiniteAdeleRing R K` is
the ring of finite adeles of `K`, defined as the restricted product of the completions
`K_v` with respect to the subrings `R_v`. Here `v` runs through the nonzero primes of `R`
and the restricted product is the subring of `∏_v K_v` consisting of elements which
are in `R_v` for all but finitely many `v`.

            ℤInt : TypeThe integers.

This type is special-cased by the compiler and overridden with an efficient implementation. The
runtime has a special representation for `Int` that stores “small” signed numbers directly, while
larger numbers use a fast arbitrary-precision arithmetic library (usually
[GMP](https://gmplib.org/)). A “small number” is an integer that can be encoded with one fewer bits
than the platform's pointer size (i.e. 63 bits on 64-bit architectures and 31 bits on 32-bit
architectures).
 ℚRat : TypeRational numbers, implemented as a pair of integers `num / den` such that the
denominator is positive and the numerator and denominator are coprime.
)),
      FiniteDimensionalFiniteDimensional.{u_1, u_2} (K : Type u_1) (V : Type u_2) [DivisionRing K] [AddCommGroup V] [Module K V] : Prop`FiniteDimensional` vector spaces are defined to be finite modules.
Use `Module.Basis.finiteDimensional_of_finite` to prove finite dimension from another definition.  ℂComplex : TypeComplex numbers consist of two `Real`s: a real part `re` and an imaginary part `im`. 
        (HasQuotient.Quotient.{u, v} (A : outParam (Type u)) {B : Type v} [self : HasQuotient A B] : B → Type (max u v)`HasQuotient.Quotient A b` (denoted as `A ⧸ b`) is the quotient of the type `A` by `b`.

This differs from `HasQuotient.quotient'` in that the `A` argument is explicit,
which is necessary to make Lean show the notation in the goal state.
↥(AutomorphicForm.GLn.ZAutomorphicForm.GLn.Z (G : Type) [TopologicalSpace G] [Group G] (E : Type) [NormedAddCommGroup E] [NormedSpace ℝ E]
  [ChartedSpace E G] [LieGroup (modelWithCornersSelf ℝ E) ⊤ G] : Subalgebra ℂ (AutomorphicForm.GLn.Alg G E)
              (GLMatrix.GeneralLinearGroup.{u, v} (n : Type u) (R : Type v) [DecidableEq n] [Fintype n] [Semiring R] : Type (max v u)`GL n R` is the group of `n` by `n` `R`-matrices with unit determinant.
Defined as a subtype of matrices  (FinFin (n : ℕ) : TypeNatural numbers less than some upper bound.

In particular, a `Fin n` is a natural number `i` with the constraint that `i < n`. It is the
canonical type with `n` elements.
 nℕ) ℝReal : TypeThe type `ℝ` of real numbers constructed as equivalence classes of Cauchy sequences of rational
numbers. )
              (MatrixMatrix.{u, u', v} (m : Type u) (n : Type u') (α : Type v) : Type (max u u' v)`Matrix m n R` is the type of matrices with entries in `R`, whose rows are indexed by `m`
and whose columns are indexed by `n`.  (FinFin (n : ℕ) : TypeNatural numbers less than some upper bound.

In particular, a `Fin n` is a natural number `i` with the constraint that `i < n`. It is the
canonical type with `n` elements.
 nℕ) (FinFin (n : ℕ) : TypeNatural numbers less than some upper bound.

In particular, a `Fin n` is a natural number `i` with the constraint that `i < n`. It is the
canonical type with `n` elements.
 nℕ)
                ℝReal : TypeThe type `ℝ` of real numbers constructed as equivalence classes of Cauchy sequences of rational
numbers. )) ⧸HasQuotient.Quotient.{u, v} (A : outParam (Type u)) {B : Type v} [self : HasQuotient A B] : B → Type (max u v)`HasQuotient.Quotient A b` (denoted as `A ⧸ b`) is the quotient of the type `A` by `b`.

This differs from `HasQuotient.quotient'` in that the `A` argument is explicit,
which is necessary to make Lean show the notation in the goal state.

          Submodule.comapSubmodule.comap.{u_1, u_3, u_5, u_7} {R : Type u_1} {R₂ : Type u_3} {M : Type u_5} {M₂ : Type u_7} [Semiring R]
  [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} (f : M →ₛₗ[σ₁₂] M₂)
  (p : Submodule R₂ M₂) : Submodule R MThe pullback of a submodule `p ⊆ M₂` along `f : M → M₂` 
            (AutomorphicForm.GLn.actionTensorCAlg'3AutomorphicForm.GLn.actionTensorCAlg'3 (G : Type) [TopologicalSpace G] [Group G] (E : Type) [NormedAddCommGroup E]
  [NormedSpace ℝ E] [ChartedSpace E G] [LieGroup (modelWithCornersSelf ℝ E) ⊤ G] :
  ↥(AutomorphicForm.GLn.Z G E) →ₐ[ℂ]
    Module.End ℂ (ContMDiffMap (modelWithCornersSelf ℝ E) (modelWithCornersSelf ℝ ℂ) G ℂ ↑⊤)
                (GLMatrix.GeneralLinearGroup.{u, v} (n : Type u) (R : Type v) [DecidableEq n] [Fintype n] [Semiring R] : Type (max v u)`GL n R` is the group of `n` by `n` `R`-matrices with unit determinant.
Defined as a subtype of matrices  (FinFin (n : ℕ) : TypeNatural numbers less than some upper bound.

In particular, a `Fin n` is a natural number `i` with the constraint that `i < n`. It is the
canonical type with `n` elements.
 nℕ) ℝReal : TypeThe type `ℝ` of real numbers constructed as equivalence classes of Cauchy sequences of rational
numbers. )
                (MatrixMatrix.{u, u', v} (m : Type u) (n : Type u') (α : Type v) : Type (max u u' v)`Matrix m n R` is the type of matrices with entries in `R`, whose rows are indexed by `m`
and whose columns are indexed by `n`.  (FinFin (n : ℕ) : TypeNatural numbers less than some upper bound.

In particular, a `Fin n` is a natural number `i` with the constraint that `i < n`. It is the
canonical type with `n` elements.
 nℕ) (FinFin (n : ℕ) : TypeNatural numbers less than some upper bound.

In particular, a `Fin n` is a natural number `i` with the constraint that `i < n`. It is the
canonical type with `n` elements.
 nℕ)
                  ℝReal : TypeThe type `ℝ` of real numbers constructed as equivalence classes of Cauchy sequences of rational
numbers. )).toLinearMapAlgHom.toLinearMap.{u, v, w} {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [Semiring A] [Semiring B]
  [Algebra R A] [Algebra R B] (φ : A →ₐ[R] B) : A →ₗ[R] BR-Alg ⥤ R-Mod 
            (AutomorphicForm.GLn.annihilatorAutomorphicForm.GLn.annihilator.{u_1, u_2, u_3} {R : Type u_1} [CommSemiring R] {M : Type u_2} [AddCommMonoid M]
  [Module R M] {N : Type u_3} [AddCommMonoid N] [Module R N] (a : M) : Submodule R (M →ₗ[R] N)
              ⟨Subtype.mk.{u} {α : Sort u} {p : α → Prop} (val : α) (property : p val) : Subtype pfun yGL (Fin n) ℝ ↦ toFunGL (Fin n) (IsDedekindDomain.FiniteAdeleRing ℤ ℚ) × GL (Fin n) ℝ → ℂ (Prod.mk.{u, v} {α : Type u} {β : Type v} (fst : α) (snd : β) : α × βConstructs a pair. This is usually written `(x, y)` instead of `Prod.mk x y`.


Conventions for notations in identifiers:

 * The recommended spelling of `(a, b)` in identifiers is `mk`.xGL (Fin n) (IsDedekindDomain.FiniteAdeleRing ℤ ℚ),Prod.mk.{u, v} {α : Type u} {β : Type v} (fst : α) (snd : β) : α × βConstructs a pair. This is usually written `(x, y)` instead of `Prod.mk x y`.


Conventions for notations in identifiers:

 * The recommended spelling of `(a, b)` in identifiers is `mk`. yGL (Fin n) ℝ)Prod.mk.{u, v} {α : Type u} {β : Type v} (fst : α) (snd : β) : α × βConstructs a pair. This is usually written `(x, y)` instead of `Prod.mk x y`.


Conventions for notations in identifiers:

 * The recommended spelling of `(a, b)` in identifiers is `mk`.,Subtype.mk.{u} {α : Sort u} {p : α → Prop} (val : α) (property : p val) : Subtype p
                ⋯⟩Subtype.mk.{u} {α : Sort u} {p : α → Prop} (val : α) (property : p val) : Subtype p))HasQuotient.Quotient.{u, v} (A : outParam (Type u)) {B : Type v} [self : HasQuotient A B] : B → Type (max u v)`HasQuotient.Quotient A b` (denoted as `A ⧸ b`) is the quotient of the type `A` by `b`.

This differs from `HasQuotient.quotient'` in that the `A` argument is explicit,
which is necessary to make Lean show the notation in the goal state.
) :
  AutomorphicForm.GLn.AutomorphicFormForGLnOverQAutomorphicForm.GLn.AutomorphicFormForGLnOverQ (n : ℕ) (ρ : AutomorphicForm.GLn.Weight n) : TypeAutomorphic forms for GL_n/Q with weight ρ. 
    nℕ ρAutomorphicForm.GLn.Weight n