Statement of Fermat's Last Theorem #

This file states Fermat's Last Theorem. We provide a statement over a general semiring with specific exponent, along with the usual statement over the naturals.

def FermatLastTheoremWith (α : Type u_1) [Semiring α] (n : ) :

Statement of Fermat's Last Theorem over a given semiring with a specific exponent.

Instances For

    Statement of Fermat's Last Theorem: a ^ n + b ^ n = c ^ n has no nontrivial integer solution when n ≥ 3.

    Instances For
      theorem FermatLastTheoremWith.mono {α : Type u_1} [Semiring α] [NoZeroDivisors α] {m : } {n : } (hmn : m n) (hm : FermatLastTheoremWith α m) :