Fermat42 — Mathlib

English

FermatLastTheoremFor n is equivalent to FermatLastTheoremWith Rat n.

Русский

FermatLastTheoremFor n эквивалентна FermatLastTheoremWith Rat n.

LaTeX

$$$FermatLastTheoremFor\\ n \\iff FermatLastTheoremWith\\ Rat\\ n$$$

Lean4

/-- Shorthand for three non-zero integers `a`, `b`, and `c` satisfying `a ^ 4 + b ^ 4 = c ^ 2`.
We will show that no integers satisfy this equation. Clearly Fermat's Last theorem for n = 4
follows. -/
def Fermat42 (a b c : ℤ) : Prop :=
  a ≠ 0 ∧ b ≠ 0 ∧ a ^ 4 + b ^ 4 = c ^ 2

Похожие утверждения