Fermat's Last Theorem in Lean 4

Namespace `UnipotentTermUnfolding` 3 theorems

Iwasawa unfolding of the unipotent term, semi-locally factorizable case UnipotentTermUnfolding.exists_forall_integrableOn_and_lintegral_ne_top_and_setIntegral_unipotentTerm_eq_mul_integral_iwasawa_of_isSemiLocalFactorization 102 below · cited by 1 · depth 29
Fibrewise finiteness of the unipotent term in Iwasawa coordinates UnipotentTermUnfolding.forall_exists_lintegral_iwasawa_tsum_tsum_enorm_sub_ne_top_of_isSemiLocalFactorization 102 below · cited by 1 · depth 29
Iwasawa unfolding of the unipotent cusp-kernel term UnipotentTermUnfolding.exists_forall_setIntegral_unipotentTerm_eq_mul_integral_iwasawa 30 below · cited by 1 · depth 30

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.