English
In the coordinate ring of a Weierstrass affine curve W' over R, the image of the constant-coefficient polynomial C applied to the addition polynomial addPolynomial(x, y, ℓ) equals the product (Y − C(linePolynomial(x, y, ℓ))) · (W'.negPolynomial − C(linePolynomial(x, y, ℓ))).
Русский
В координатном кольце аффинной кривой Вейерштрасса W' над R образ константной полиномиальной функции C, применённой к полиному addPolynomial(x, y, ℓ), равен произведению (Y − C(linePolynomial(x, y, ℓ))) · (W'.negPolynomial − C(linePolynomial(x, y, ℓ))).
LaTeX
$$$mk\,W'\Big(C\big(W'.addPolynomial\,x\,y\,\ell\big)\Big) = mk\,W'\big(\big(Y - C\big(linePolynomial\,x\,y\,\ell\big)\big) \cdot \big(W'.negPolynomial - C\big(linePolynomial\,x\,y\,\ell\big)\big)\big)$$$
Lean4
theorem C_addPolynomial (x y ℓ : R) :
mk W' (C <| W'.addPolynomial x y ℓ) =
mk W' ((Y - C (linePolynomial x y ℓ)) * (W'.negPolynomial - C (linePolynomial x y ℓ))) :=
AdjoinRoot.mk_eq_mk.mpr ⟨1, by rw [W'.C_addPolynomial, add_sub_cancel_left, mul_one]⟩
