### Action of GLn(AQf) on Automorphic Forms

Source: https://imperialcollegelondon.github.io/FLT/blueprint/sect0004.html

Demonstrates the left action of the group GLn(AQf) on the space of automorphic forms for GLn(AQ) by the formula (g⋅f)(x,y)=f(xg,y).

```Lean
(g⋅f)(x,y)=f(xg,y)
```

--------------------------------

### Automorphic Form Definition for GLn Over Q

Source: https://imperialcollegelondon.github.io/FLT/blueprint/sect0004.html

Defines a smooth function f: GLn(AQf) x GLn(R) -> C as an On(R)-automorphic form on GLn(AQ) if it satisfies periodicity, finite level, weight, infinite level, and growth conditions.

```Lean
AutomorphicForm.GLn.AutomorphicFormForGLnOverQ
```

--------------------------------

### Lean Declarations for Haar Characters

Source: https://imperialcollegelondon.github.io/FLT/blueprint/Haar_char_project.html

A list of Lean declarations related to Haar characters and their properties.

```Lean
MeasureTheory.addEquivAddHaarChar
```

```Lean
MeasureTheory.addEquivAddHaarChar_eq
```

```Lean
MeasureTheory.addEquivAddHaarChar_smul_map
```

```Lean
MeasureTheory.addEquivAddHaarChar_smul_eq_comap
```

```Lean
MeasureTheory.addEquivAddHaarChar_smul_preimage
```

```Lean
MeasureTheory.addEquivAddHaarChar_smul_integral_map
```