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`. 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) ℝ) : ℝAn auxiliary "size" function on invertible real matrices used in the slowly
increasing condition; namely `tr(MMᵀ) + tr(M⁻¹(M⁻¹)ᵀ)`.  ↑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ℕ

wAutomorphicForm.GLn.preweight nThe underlying preweight, i.e. continuous representation of `O(n)`.  : AutomorphicForm.GLn.preweightAutomorphicForm.GLn.preweight (n : ℕ) : TypeA preweight for `GLₙ` is a continuous representation of the real orthogonal
group `O(n)` on a finite-dimensional complex vector space.  nℕ

The underlying preweight, i.e. continuous representation of `O(n)`. 

isSimpleCategoryTheory.Simple (AutomorphicForm.GLn.preweight.fdRep n self.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) ℝ)The finite-dimensional `ℂ`-representation of `O(n)` associated to a preweight `w`.  nℕ selfAutomorphicForm.GLn.Weight n.wAutomorphicForm.GLn.Weight.w {n : ℕ} (self : AutomorphicForm.GLn.Weight n) : AutomorphicForm.GLn.preweight nThe underlying preweight, i.e. continuous representation of `O(n)`. )

toFunGL (Fin n) (IsDedekindDomain.FiniteAdeleRing ℤ ℚ) × GL (Fin n) ℝ → ℂThe underlying function `GL_n(𝔸_f) × GL_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`. 

The underlying function `GL_n(𝔸_f) × GL_n(ℝ) → ℂ`. 

is_smoothAutomorphicForm.GLn.IsSmooth self.toFun : AutomorphicForm.GLn.IsSmoothAutomorphicForm.GLn.IsSmooth {n : ℕ} (f : GL (Fin n) (IsDedekindDomain.FiniteAdeleRing ℤ ℚ) × GL (Fin n) ℝ → ℂ) : PropA function on `GL_n(𝔸_f) × GL_n(ℝ)` is smooth if it is continuous, locally constant
in the finite-adelic variable, and `C^∞` in the archimedean variable.  selfAutomorphicForm.GLn.AutomorphicFormForGLnOverQ n ρ.toFunAutomorphicForm.GLn.AutomorphicFormForGLnOverQ.toFun {n : ℕ} {ρ : AutomorphicForm.GLn.Weight n}
  (self : AutomorphicForm.GLn.AutomorphicFormForGLnOverQ n ρ) :
  GL (Fin n) (IsDedekindDomain.FiniteAdeleRing ℤ ℚ) × GL (Fin n) ℝ → ℂThe underlying function `GL_n(𝔸_f) × GL_n(ℝ) → ℂ`. 

is_periodic∀ (g : GL (Fin n) ℚ) (x : GL (Fin n) (IsDedekindDomain.FiniteAdeleRing ℤ ℚ)) (y : GL (Fin n) ℝ),
  self.toFun
      (((algebraMap ℚ (IsDedekindDomain.FiniteAdeleRing ℤ ℚ)).GL (Fin n)) g * x, ((algebraMap ℚ ℝ).GL (Fin n)) g * y) =
    self.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. ),
  selfAutomorphicForm.GLn.AutomorphicFormForGLnOverQ n ρ.toFunAutomorphicForm.GLn.AutomorphicFormForGLnOverQ.toFun {n : ℕ} {ρ : AutomorphicForm.GLn.Weight n}
  (self : AutomorphicForm.GLn.AutomorphicFormForGLnOverQ n ρ) :
  GL (Fin n) (IsDedekindDomain.FiniteAdeleRing ℤ ℚ) × GL (Fin n) ℝ → ℂThe underlying function `GL_n(𝔸_f) × GL_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`.((algebraMapAlgebra.algebraMap.{u, v} (R : Type u) (A : Type v) {inst✝ : CommSemiring R} {inst✝¹ : Semiring A}
  [self : 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 BFunctoriality of `GLₘ`: a ring homomorphism `A →+* B` induces a group homomorphism
`GLₘ(A) →* GLₘ(B)` by applying it entrywise.  (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`. ((algebraMapAlgebra.algebraMap.{u, v} (R : Type u) (A : Type v) {inst✝ : CommSemiring R} {inst✝¹ : Semiring A}
  [self : 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 BFunctoriality of `GLₘ`: a ring homomorphism `A →+* B` induces a group homomorphism
`GLₘ(A) →* GLₘ(B)` by applying it entrywise.  (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`.
    selfAutomorphicForm.GLn.AutomorphicFormForGLnOverQ n ρ.toFunAutomorphicForm.GLn.AutomorphicFormForGLnOverQ.toFun {n : ℕ} {ρ : AutomorphicForm.GLn.Weight n}
  (self : AutomorphicForm.GLn.AutomorphicFormForGLnOverQ n ρ) :
  GL (Fin n) (IsDedekindDomain.FiniteAdeleRing ℤ ℚ) × GL (Fin n) ℝ → ℂThe underlying function `GL_n(𝔸_f) × GL_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 ↦ self.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) ℝ → ℂ) : PropA function `f : GL_n(ℝ) → ℂ` is slowly increasing if there exist `C, N` such
that `‖f M‖ ≤ C · s(M)^N` for all `M`, where `s` is an auxiliary "size" function.  fun yGL (Fin n) ℝ ↦ selfAutomorphicForm.GLn.AutomorphicFormForGLnOverQ n ρ.toFunAutomorphicForm.GLn.AutomorphicFormForGLnOverQ.toFun {n : ℕ} {ρ : AutomorphicForm.GLn.Weight n}
  (self : AutomorphicForm.GLn.AutomorphicFormForGLnOverQ n ρ) :
  GL (Fin n) (IsDedekindDomain.FiniteAdeleRing ℤ ℚ) × GL (Fin n) ℝ → ℂThe underlying function `GL_n(𝔸_f) × GL_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 self.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) ℝ → ℂ) : PropThe function `f : GL_n(𝔸_f) × GL_n(ℝ) → ℂ` is right-`U`-invariant in the
finite-adelic variable, where `U` is an open compact subgroup.  USubgroup (GL (Fin n) (IsDedekindDomain.FiniteAdeleRing ℤ ℚ)) selfAutomorphicForm.GLn.AutomorphicFormForGLnOverQ n ρ.toFunAutomorphicForm.GLn.AutomorphicFormForGLnOverQ.toFun {n : ℕ} {ρ : AutomorphicForm.GLn.Weight n}
  (self : AutomorphicForm.GLn.AutomorphicFormForGLnOverQ n ρ) :
  GL (Fin n) (IsDedekindDomain.FiniteAdeleRing ℤ ℚ) × GL (Fin n) ℝ → ℂThe underlying function `GL_n(𝔸_f) × GL_n(ℝ) → ℂ`.