English
The cubic Weierstrass relation in projective coordinates expresses the sum of the three coordinate polynomials weighted by the projective coordinates equalling the projective evaluation of the overall cubic.
Русский
Кубическое уравнение Вейерштрасса в проективных координатах выражает сумму трёх координатных многочленов, взвешенных проективными координатами, равной значению всей кубической части.
LaTeX
$$$3 \\cdot (\\mathrm{eval}\\;P\\, W'.polynomial) = P x \\cdot (\\mathrm{eval}\\;P\\, W'.polynomialX) + P y \\cdot (\\mathrm{eval}\\;P\\, W'.polynomialY) + P z \\cdot (\\mathrm{eval}\\;P\\, W'.polynomialZ)$$$
Lean4
/-- The proposition that a projective 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)
