English
The nonsingularity condition is equivalent to the conjunction of the curve equation and a nonvanishing among the X, Y, Z evaluations.
Русский
Условие неособримости эквивалентно сочетанию уравнения кривой и ненулевости хотя бы одного из X, Y, Z в точке.
LaTeX
$$$ W'.Nonsingular P \\leftrightarrow 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
theorem nonsingular_iff (P : Fin 3 → R) :
W'.Nonsingular P ↔
W'.Equation P ∧
(W'.a₁ * P y * P z - (3 * P x ^ 2 + 2 * W'.a₂ * P x * P z ^ 2 + W'.a₄ * P z ^ 4) ≠ 0 ∨
2 * P y + W'.a₁ * P x * P z + W'.a₃ * P z ^ 3 ≠ 0 ∨
W'.a₁ * P x * P y + 3 * W'.a₃ * P y * P z ^ 2 -
(2 * W'.a₂ * P x ^ 2 * P z + 4 * W'.a₄ * P x * P z ^ 3 + 6 * W'.a₆ * P z ^ 5) ≠
0) :=
by rw [Nonsingular, eval_polynomialX, eval_polynomialY, eval_polynomialZ]
