English
The Jacobian definition of nonsingularity for a representative P requires that the Jacobian equation is satisfied and at least one of the partial evaluations of X, Y, Z is nonzero.
Русский
Для представителя P на Якобиане требуется, чтобы выполнялось уравнение Якобиана и хотя бы одно из значений X, Y, Z не равно нулю.
LaTeX
$$$ W'.Nonsingular P := W'.Equation P \\wedge ( \\mathrm{eval} P\\,W'.polynomialX \\neq 0 \\lor \\mathrm{eval} P\\,W'.polynomialY \\neq 0 \\lor \\mathrm{eval} P\\,W'.polynomialZ \\neq 0 )$$$
Lean4
/-- The proposition that a Jacobian point representative `(x, y, z)` on a Weierstrass curve `W` is
nonsingular.
In other words, either `W_X(x, y, z) ≠ 0`, `W_Y(x, y, z) ≠ 0`, or `W_Z(x, y, z) ≠ 0`.
Note that this definition is only mathematically accurate for fields. -/
-- TODO: generalise this definition to be mathematically accurate for a larger class of rings.
def Nonsingular (P : Fin 3 → R) : Prop :=
W'.Equation P ∧ (eval P W'.polynomialX ≠ 0 ∨ eval P W'.polynomialY ≠ 0 ∨ eval P W'.polynomialZ ≠ 0)
