minimal_comm — Mathlib

English

If a,b,c form a minimal solution, then swapping a and b yields another minimal solution.

Русский

Если (a,b,c) образуют минимальное решение, то перенос a и b даст другое минимальное решение.

LaTeX

$$$Fermat42.Minimal\\ a\\ b\\ c \\rightarrow Fermat42.Minimal\\ b\\ a\\ c$$$

Lean4

/-- We can swap `a` and `b` in a minimal solution to `a ^ 4 + b ^ 4 = c ^ 2`. -/
theorem minimal_comm {a b c : ℤ} : Minimal a b c → Minimal b a c := fun ⟨h1, h2⟩ => ⟨Fermat42.comm.mp h1, h2⟩

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