exists_Solution_multiplicity_lt — Mathlib

English

There exists a minimal S such that the descent procedure yields a contradiction, proving the three-dimensional Fermat’s Last Theorem.

Русский

Существует минимальное решение, для которого нисхождение приводит к противоречию, доказывая теорему Ферма о несуществовании трёх натуральных чисел.

LaTeX

$$def fermatLastTheoremThree := FermatLastTheoremForThree_of_FermatLastTheoremThreeGen …$$

Lean4

/-- Given any `S : Solution`, there is another `S₁ : Solution` such that
  `S₁.multiplicity < S.multiplicity` -/
theorem exists_Solution_multiplicity_lt : ∃ S₁ : Solution hζ, S₁.multiplicity < S.multiplicity := by
  classical
  obtain ⟨S', hS'⟩ := exists_Solution_of_Solution' (Solution'_descent S)
  exact ⟨S', hS' ▸ Solution'_descent_multiplicity_lt S⟩

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