English
A weakened variant FermatLastTheoremWith' over a commutative semiring asserts that whenever a^n + b^n = c^n with nonzero a,b,c, there exist d, a', b', c' with a = a' d, b = b' d, c = c' d and a', b', c' are units.
Русский
Упрощённая версия FermatLastTheoremWith' над коммутативной полуполь Ring требует, чтобы любые не нулевые решения x^n + y^n = z^n распадались на общие множители и единицы в частях.
LaTeX
$$$FermatLastTheoremWith'\\ R\\ n := \\forall a,b,c\\in R,\\ a \\neq 0 \\to b \\neq 0 \\to c \\neq 0 \\to a^n + b^n = c^n \\to \\exists d,a',b',c',\\ (a = a' d \\land b = b' d \\land c = c' d) \\land (IsUnit a' \\land IsUnit b' \\land IsUnit c')$$$
Lean4
/-- A relaxed variant of Fermat's Last Theorem over a given commutative semiring with a specific
exponent, allowing nonzero solutions of units and their common multiples.
1. The variant `FermatLastTheoremWith' R` is weaker than `FermatLastTheoremWith R` in general.
In particular, it holds trivially for `[Field R]`.
2. This variant is equivalent to the original `FermatLastTheoremWith R` for `R = ℕ` or `ℤ`.
In general, they are equivalent if there is no solutions of units to the Fermat equation.
3. For a polynomial ring `R = k[X]`, the original `FermatLastTheoremWith R` is false but the weaker
variant `FermatLastTheoremWith' R` is true. This polynomial variant of Fermat's Last Theorem
can be shown elementarily using Mason--Stothers theorem.
-/
def FermatLastTheoremWith' (R : Type*) [CommSemiring R] (n : ℕ) : Prop :=
∀ a b c : R,
a ≠ 0 →
b ≠ 0 →
c ≠ 0 →
a ^ n + b ^ n = c ^ n →
∃ d a' b' c', (a = a' * d ∧ b = b' * d ∧ c = c' * d) ∧ (IsUnit a' ∧ IsUnit b' ∧ IsUnit c')
