Fermat's Last Theorem in Lean 4

Namespace `EulerProduct` 3 theorems

Logarithmic derivative of an absolutely convergent Euler product EulerProduct.differentiableAt_and_ne_zero_and_hasSum_log_mul_div_neg_deriv_tprod_div 0 below · cited by 3 · depth 29
Euler product bounded by exp(2sum Nᵢ^{-Res}) EulerProduct.norm_tprod_inv_one_sub_mul_natCast_cpow_neg_le_exp 0 below · cited by 4 · depth 30
The 3–4–1 inequality for Euler products EulerProduct.three_mul_re_neg_deriv_tprod_div_add_four_mul_add_nonneg_of_norm_le_one 0 below · cited by 2 · 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.