Fermat's Last Theorem in Lean 4

Namespace `LocalGroupLaw` 3 theorems

Local exponential of a holomorphic commutative local group law LocalGroupLaw.exists_localExp_of_differentiableOn_of_comm_of_assoc 2 below · cited by 1 · depth 30
A local homomorphism factors through a local exponential LocalGroupLaw.exists_ball_eq_localExp_comp_fderiv_of_map_add 2 below · cited by 1 · depth 32
Holomorphic local exponential for a family of commutative local group laws LocalGroupLaw.exists_localExp_family_of_differentiableOn_of_comm_of_assoc 2 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.