neg_of_minimal — Mathlib

English

If (a,b,c) is minimal, then (a,b,-c) is also minimal.

Русский

Если (a,b,c) минимально, то (a,b,-c) тоже минимально.

LaTeX

$$$Fermat42.Minimal\\ a\\ b\\ c \\rightarrow Fermat42.Minimal\\ a\\ b\\ (-c)$$$

Lean4

/-- We can assume that a minimal solution to `a ^ 4 + b ^ 4 = c ^ 2` has positive `c`. -/
theorem neg_of_minimal {a b c : ℤ} : Minimal a b c → Minimal a b (-c) :=
  by
  rintro ⟨⟨ha, hb, heq⟩, h2⟩
  constructor
  · apply And.intro ha (And.intro hb _)
    rw [heq]
    exact (neg_sq c).symm
  rwa [Int.natAbs_neg c]

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