English
Let W' be the Jacobian of a Weierstrass curve over a commutative ring. A point on the Jacobian is given by a triple P = (x, y, z) in Fin(3) → R. This triple lies on the Weierstrass curve W if and only if the homogeneous Weierstrass equation W(X, Y, Z) = 0 is satisfied when X = x, Y = y, Z = z.
Русский
Пусть W' является Якобианом кривой Вейерштрасса над кольцом R. Тройка P = (x, y, z) задаёт точку на Якобиане. Точка лежит на кривой Вейерштрасса W тогда и только тогда, когда однородное уравнение Вейерштрасса W(X, Y, Z) = 0 выполняется при X = x, Y = y, Z = z.
LaTeX
$$$W'.Equation(P) \\iff \\operatorname{eval}_P(W'.polynomial) = 0$$$
Lean4
/-- The proposition that a Jacobian point representative `(x, y, z)` lies in a Weierstrass curve
`W`.
In other words, it satisfies the `(2, 3, 1)`-homogeneous Weierstrass equation `W(X, Y, Z) = 0`. -/
def Equation (P : Fin 3 → R) : Prop :=
eval P W'.polynomial = 0
