English
There is a noncomputable descent mapping from S to S.Solution'_descent.
Русский
Существование нисходящего отображения S → S.Solution'_descent.
LaTeX
$$exists_Solution'_descent : Solution'_descent S$$
Lean4
/-- Given `S : Solution`, we construct `S₁ : Solution'`, with smaller multiplicity of `λ` in
`c` (see `Solution'_descent_multiplicity_lt` below.). -/
noncomputable def Solution'_descent : Solution' hζ where
a := S.Y
b := S.u₄ * S.Z
c := λ ^ (S.multiplicity - 1) * S.X
u := S.u₅
ha := S.lambda_not_dvd_Y
hb := fun h ↦ S.lambda_not_dvd_Z <| Units.dvd_mul_left.1 h
hc := fun h ↦ S.X_ne_zero <| by simpa [hζ.zeta_sub_one_prime'.ne_zero] using h
coprime := (isCoprime_mul_unit_left_right S.u₄.isUnit _ _).2 S.isCoprime_Y_Z
hcdvd := by
refine dvd_mul_of_dvd_left (dvd_pow_self _ (fun h ↦ ?_)) _
rw [Nat.sub_eq_iff_eq_add (le_trans (by simp) S.two_le_multiplicity), zero_add] at h
simpa [h] using S.two_le_multiplicity
H := formula3 S
