exists_Solution_of_Solution' — Mathlib

English

There exists a Solution S1 whose multiplicity matches that of S'.

Русский

Существует решение S1, чья кратность совпадает с кратностью S'.

LaTeX

$$$\exists S_1 \;\text{such that } S_1.multiplicity = S'.multiplicity$$$

Lean4

/-- Given `S' : Solution'`, then there is `S₁ : Solution` such that
`S₁.multiplicity = S'.multiplicity`. -/
theorem exists_Solution_of_Solution' : ∃ (S₁ : Solution hζ), S₁.multiplicity = S'.multiplicity :=
  by
  obtain ⟨a, b, H, coprime, ha, hb, hab⟩ := ex_cube_add_cube_eq_and_isCoprime_and_not_dvd_and_dvd S'
  exact
    ⟨{  a := a
        b := b
        c := S'.c
        u := S'.u
        ha := ha
        hb := hb
        hc := S'.hc
        coprime := coprime
        hcdvd := S'.hcdvd
        H := H
        hab := hab }, rfl⟩

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