Lean Proof of Fermat's Last Theorem

https://imperialcollegelondon.github.io/FLT/blueprint/

Admin

A formal verification project documenting the path towards a complete Lean proof of Fermat's Last...

Tokens:28,800

Snippets:453

Trust Score:9.7

Update:6 months ago

Show doc for...

Tokens:

Raw

### 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
```

Tokens:

Raw