fermatLastTheoremWith'_of_semifield

English

For each natural n, the trio FermatLastTheoremFor n, FermatLastTheoremWith' Nat n, and FermatLastTheoremWith' Int n are mutually equivalent (TFAE).

Русский

Для каждого натурального n три высказывания FermatLastTheoremFor n, FermatLastTheoremWith' Nat n и FermatLastTheoremWith' Int n взаимно эквивалентны (TFAE).

LaTeX

$$$\\forall n \\in \\mathbb{N},\\ (FermatLastTheoremFor\\ n) \\iff (FermatLastTheoremWith'\\ Nat\\ n) \\iff (FermatLastTheoremWith'\\ Int\\ n)$$$

Lean4

theorem fermatLastTheoremWith'_of_semifield (𝕜 : Type*) [Semifield 𝕜] (n : ℕ) : FermatLastTheoremWith' 𝕜 n :=
  fun a b c ha hb hc _ ↦
  ⟨1, a, b, c, ⟨(mul_one a).symm, (mul_one b).symm, (mul_one c).symm⟩, ⟨ha.isUnit, hb.isUnit, hc.isUnit⟩⟩

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