English
For any semifield 𝕜 and any n, FermatLastTheoremWith' 𝕜 n holds because every nonzero element is a unit in a semifield.
Русский
Для любого полуделимого тела 𝕜 и любого n верна версия FermatLastTheoremWith' 𝕜 n, так как в полуделимом теле каждое ненулевое число является единицей.
LaTeX
$$$\\forall \\mathbb{K}\\, [\\text{Semifield } \\mathbb{K}]\\, (n:\\ mathbb{N}),\\ FermatLastTheoremWith'\\mathbb{K}\\\\mathit{n}$$$
Lean4
theorem fermatLastTheoremWith {R : Type*} [CommSemiring R] [IsDomain R] {n : ℕ} (h : FermatLastTheoremWith' R n)
(hn : ∀ a b c : R, IsUnit a → IsUnit b → IsUnit c → a ^ n + b ^ n ≠ c ^ n) : FermatLastTheoremWith R n :=
by
intro a b c ha hb hc heq
rcases h a b c ha hb hc heq with ⟨d, a', b', c', ⟨rfl, rfl, rfl⟩, ⟨ua, ub, uc⟩⟩
rw [mul_pow, mul_pow, mul_pow, ← add_mul] at heq
exact hn _ _ _ ua ub uc <| mul_right_cancel₀ (pow_ne_zero _ (right_ne_zero_of_mul ha)) heq
