addPolynomial — Mathlib

English

If x1 ≠ x2, the slope is given by (y1 − y2)/(x1 − x2).

Русский

Если x1 ≠ x2, наклон определяется как (y1 − y2)/(x1 − x2).

LaTeX

$$$x_1 \neq x_2 \Rightarrow W.slope x_1 x_2 y_1 y_2 = (y_1 - y_2)/(x_1 - x_2)$$$

Lean4

/-- The addition polynomial obtained by substituting the line `Y = ℓ(X - x) + y` into the polynomial
`W(X, Y)` associated to a Weierstrass curve `W`. If such a line intersects `W` at another
nonsingular affine point `(x', y')` on `W`, then the roots of this polynomial are precisely `x`,
`x'`, and the `X`-coordinate of the addition of `(x, y)` and `(x', y')`.

This depends on `W`, and has argument order: `x`, `y`, `ℓ`. -/
noncomputable def addPolynomial (x y ℓ : R) : R[X] :=
  W'.polynomial.eval <| linePolynomial x y ℓ

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