FermatLastTheoremForThreeGen — Mathlib

English

If S' is a Solution', then λ^4 divides S'.c^3.

Русский

Если S' является Solution', то λ^4 делит S'.c^3.

LaTeX

$$$\lambda^4 \mid S'.c^3$$$

Lean4

/-- `FermatLastTheoremForThreeGen` is the statement that `a ^ 3 + b ^ 3 = u * c ^ 3` has no
nontrivial solutions in `𝓞 K` for all `u : (𝓞 K)ˣ` such that `¬ λ ∣ a`, `¬ λ ∣ b` and `λ ∣ c`.
The reason to consider `FermatLastTheoremForThreeGen` is to make a descent argument working. -/
def FermatLastTheoremForThreeGen : Prop :=
  ∀ a b c : 𝓞 K, ∀ u : (𝓞 K)ˣ, c ≠ 0 → ¬λ ∣ a → ¬λ ∣ b → λ ∣ c → IsCoprime a b → a ^ 3 + b ^ 3 ≠ u * c ^ 3

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