Fermat's Last Theorem for regular primes

Source: url:https://github.com/leanprover-community/flt-regular Authors: FltRegular contributors Status: verified Main declarations: flt_regular Tags: algebraic-number-theory, fermats-last-theorem, cyclotomic-fields, class-groups, regular-primes MSC: 11D41, 11R18, 11R29