Fermat's Last Theorem in Lean 4

Namespace `GlobalGaloisRep` 3 theorems

— 1 · IsUnramifiedAt 2

directly in `GlobalGaloisRep` 1

Open-kernel representations of G_ℚ are almost everywhere unramified GlobalGaloisRep.exists_finset_forall_isUnramifiedAt_of_isOpen_ker 1 below · cited by 3 · depth 11

`GlobalGaloisRep.IsUnramifiedAt` 2

Unramifiedness at q transfers from places to primes of 𝒪_F GlobalGaloisRep.IsUnramifiedAt.algebraIsUnramifiedAt_of_ker_le_fixingSubgroup 2 below · cited by 2 · depth 10
Frobenius images at an unramified prime agree up to conjugacy GlobalGaloisRep.IsUnramifiedAt.exists_apply_eq_apply_conj_of_isFrobeniusAt 2 below · cited by 4 · depth 11

Documents the Lean sources in this repository (Lean v4.33.1, Mathlib v4.33.0). Statements are quoted textually from the .lean files; dependency edges are the import Theorems.Thm_… lines of the proof modules. About these pages.