English
The slope of the mapped affine Weierstrass curve is the image under f of the slope of the original curve, for all x1,x2,y1,y2 in F.
Русский
Уклон наобразной аффинной кривой Вейерштрасса есть образ уклона исходной кривой через f.
LaTeX
$$$ (W.map f).toAffine.slope (f x_1) (f x_2) (f y_1) (f y_2) = f (W.slope x_1 x_2 y_1 y_2) $$$
Lean4
theorem map_slope [DecidableEq F] [DecidableEq K] (f : F →+* K) (x₁ x₂ y₁ y₂ : F) :
(W.map f).toAffine.slope (f x₁) (f x₂) (f y₁) (f y₂) = f (W.slope x₁ x₂ y₁ y₂) :=
by
by_cases hx : x₁ = x₂
· by_cases hy : y₁ = W.negY x₂ y₂
· rw [slope_of_Y_eq (congr_arg f hx) <| by rw [hy, map_negY], slope_of_Y_eq hx hy, map_zero]
· rw [slope_of_Y_ne (congr_arg f hx) <| map_negY f x₂ y₂ ▸ fun h => hy <| f.injective h, map_negY,
slope_of_Y_ne hx hy]
map_simp
· rw [slope_of_X_ne fun h => hx <| f.injective h, slope_of_X_ne hx]
map_simp
