Fermat's Last Theorem in Lean 4

Namespace `Finset` 2 theorems

Alternating sum over ordered chains recovers the total sum Finset.sum_neg_one_pow_mul_sum_strictMono_sum_ite_eq_sum 0 below · cited by 1 · depth 35
A q-point subset of the box misses an invertible completion Finset.exists_mem_and_not_mem_and_isUnit_sub_mul_of_card_eq_of_prime 0 below · cited by 1 · depth 37

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.