English
If the principal coordinate Z of P is zero, then W′.Nonsingular P is equivalent to P satisfying the curve equation together with a non-vanishing condition derived from the x- and y-coordinates (and the Weierstrass coefficients).
Русский
Если координата Z тройки P равна нулю, то несингулярность W′ при P эквивалентна тому, что P удовлетворяет уравнению кривой вместе с условием, что определенные выражения не равны нулю (с учетом коэффициентов кривой).
LaTeX
$$$P: \\mathrm{Fin}(3)\\to R,\\; h_Pz:\\ P_z=0 \\;\\Longrightarrow\\; W'.Nonsingular P \\iff (W'.Equation P \\land (3P_x^2 \\neq 0 \\lor P_y^2 + W'.a_1 P_x P_y - W'.a_2 P_x^2 \\neq 0))$$$
Lean4
theorem nonsingular_of_Z_eq_zero {P : Fin 3 → R} (hPz : P z = 0) :
W'.Nonsingular P ↔ W'.Equation P ∧ (3 * P x ^ 2 ≠ 0 ∨ P y ^ 2 + W'.a₁ * P x * P y - W'.a₂ * P x ^ 2 ≠ 0) := by
simp only [nonsingular_iff, hPz, add_zero, zero_sub, mul_zero, zero_pow <| OfNat.ofNat_ne_zero _, neg_ne_zero,
ne_self_iff_false, false_or]
