Fermat's Last Theorem in Lean 4

Namespace `AddChar` 2 theorems

Continuous circle characters of a real normed space AddChar.exists_continuousLinearMap_fourierChar_eq 0 below · cited by 2 · depth 17
Simultaneous diagonalisation of an additive character by idempotents AddChar.exists_completeOrthogonalIdempotents_forall_mul_eq_pow_mul_of_forall_isUnit_one_sub_pow 1 below · cited by 1 · depth 32

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.