Minimal — Mathlib

English

Minimal a b c means that a^4 + b^4 = c^2 and c has minimal absolute value among all solutions.

Русский

Minimal a b c означает, что a^4 + b^4 = c^2 и |c| минимально среди всех решений.

LaTeX

$$$Fermat42.Minimal\\ (a,b,c) := Fermat42\\ a\\ b\\ c \\wedge \\forall a',b',c',\\ Fermat42\\ a'\\ b'\\ c' \\rightarrow |c| \\le |c'|$$$

Lean4

/-- We say a solution to `a ^ 4 + b ^ 4 = c ^ 2` is minimal if there is no other solution with
a smaller `c` (in absolute value). -/
def Minimal (a b c : ℤ) : Prop :=
  Fermat42 a b c ∧ ∀ a1 b1 c1 : ℤ, Fermat42 a1 b1 c1 → Int.natAbs c ≤ Int.natAbs c1

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