English
FermatLastTheoremFor 0 holds: there are no nonzero a,b,c ∈ ℕ with a^0 + b^0 = c^0.
Русский
Ферматова теорема для экспоненты 0 верна: не существует ненулевых a, b, c ∈ ℕ таких, что a^0 + b^0 = c^0.
LaTeX
$$$\text{FermatLastTheoremFor}(0)\;\equiv\; \forall a,b,c \in \mathbb{N}, a\neq 0, b\neq 0, c\neq 0 \Rightarrow a^0 + b^0 \neq c^0.$$$
Lean4
/-- Statement of Fermat's Last Theorem: `a ^ n + b ^ n = c ^ n` has no nontrivial natural solution
when `n ≥ 3`.
This is now a theorem of Wiles and Taylor--Wiles; see
https://github.com/ImperialCollegeLondon/FLT for an ongoing Lean formalisation of
a proof. -/
def FermatLastTheorem : Prop :=
∀ n ≥ 3, FermatLastTheoremFor n
