English
The addition polynomial W'.addPolynomial x y ℓ is exactly minus a cubic-to-poly conversion of a 4-tuple of coefficients determined by the Weierstrass data of W'.
Русский
Полином сложения W'.addPolynomial x y ℓ равен минус преобразованию кубической полиномиальной записи, чьи коэффициенты задаются данными кривой W'.
LaTeX
$$W'.addPolynomial x y ℓ = -\mathrm{Cubic.toPoly}\langle 1, -\ell^{2} - W'.a_1 \ell + W'.a_2, 2 x \ell^{2} + (W'.a_1 x - 2 y - W'.a_3) \ell + (-W'.a_1 y + W'.a_4), -x^{2} \ell^{2} + (2 x y + W'.a_3 x) \ell - (y^{2} + W'.a_3 y - W'.a_6)\rangle$$
Lean4
theorem addPolynomial_eq (x y ℓ : R) :
W'.addPolynomial x y ℓ =
-Cubic.toPoly
⟨1, -ℓ ^ 2 - W'.a₁ * ℓ + W'.a₂, 2 * x * ℓ ^ 2 + (W'.a₁ * x - 2 * y - W'.a₃) * ℓ + (-W'.a₁ * y + W'.a₄),
-x ^ 2 * ℓ ^ 2 + (2 * x * y + W'.a₃ * x) * ℓ - (y ^ 2 + W'.a₃ * y - W'.a₆)⟩ :=
by
rw [addPolynomial, linePolynomial, polynomial, Cubic.toPoly]
eval_simp
C_simp
ring1
