Standalone Lean project
A formal proof of Fermat's Last Theorem for regular prime exponents.
Flagship declarations
dvd_card_classGroup_of_unramified_isCyclic
Plain-language statement
This is the second part of Hilbert Theorem 94, which states that if L/K is an unramified cyclic finite extension of number fields of odd prime degree, then the degree divides the class number of K.
Source project: FLT for regular primes
Person-level attribution pending.
eq_pow_prime_of_unit_of_congruent
Plain-language statement
A regular prime criterion: if a unit of the cyclotomic field is congruent to an integer modulo p, then it is a p-th power.
Source project: FLT for regular primes
Person-level attribution pending.
FltRegular.caseI_easier
Plain-language statement
Case I with additional assumptions.
Source project: FLT for regular primes
Person-level attribution pending.
FltRegular.caseII
Plain-language statement
Case II of Fermat's Last Theorem for regular primes.
Source project: FLT for regular primes
Person-level attribution pending.