English
If x1 ≠ x2, the slope is (y1 − y2)/(x1 − x2); if x1 = x2 and y1 ≠ -y2 − a1 x2 − a3, the slope is the tangent slope; otherwise, slope is 0.
Русский
Если x1 ≠ x2, наклон равен (y1 − y2)/(x1 − x2); если x1 = x2 и y1 ≠ -y2 − a1 x2 − a3, наклон касательный; иначе наклон равен 0.
LaTeX
$$$W.slope x_1 x_2 y_1 y_2 = \begin{cases} \dfrac{y_1 - y_2}{x_1 - x_2}, & x_1 \neq x_2, \\ \dfrac{3 x_1^2 + 2 a_2 x_1 + a_4 - a_1 y_1}{y_1 - (-y_1 - a_1 x_1 - a_3)}, & x_1 = x_2, \text{ otherwise } 0. \end{cases}$$$
Lean4
/-- The slope of the line through two nonsingular affine points `(x₁, y₁)` and `(x₂, y₂)` on a
Weierstrass curve `W`.
If `x₁ ≠ x₂`, then this line is the secant of `W` through `(x₁, y₁)` and `(x₂, y₂)`, and has slope
`(y₁ - y₂) / (x₁ - x₂)`. Otherwise, if `y₁ ≠ -y₁ - a₁x₁ - a₃`, then this line is the tangent of `W`
at `(x₁, y₁) = (x₂, y₂)`, and has slope `(3x₁² + 2a₂x₁ + a₄ - a₁y₁) / (2y₁ + a₁x₁ + a₃)`. Otherwise,
this line is vertical, in which case this returns the value `0`.
This depends on `W`, and has argument order: `x₁`, `x₂`, `y₁`, `y₂`. -/
def slope (x₁ x₂ y₁ y₂ : F) : F :=
if x₁ = x₂ then if y₁ = W.negY x₂ y₂ then 0 else (3 * x₁ ^ 2 + 2 * W.a₂ * x₁ + W.a₄ - W.a₁ * y₁) / (y₁ - W.negY x₁ y₁)
else (y₁ - y₂) / (x₁ - x₂)
