English
Given P with nonzero Z, the nonsingularity of W at P is equivalent to the curve equation holding at P and a nonvanishing condition involving X and Y coordinates.
Русский
При заданной непустой координате Z несингулярность W в P эквивалентна выполнению уравнения кривой в P и условию, что выражения на X и Y не обращаются в ноль.
LaTeX
$$$P:\\mathrm{Fin}(3)\\to F,\\; P_z\\neq 0 \\Rightarrow W.Nonsingular P \\iff (W.Equation P \\land (\\operatorname{eval}_P W.polynomialX \\neq 0 \\lor \\operatorname{eval}_P W.polynomialY \\neq 0))$$$
Lean4
theorem nonsingular_iff_of_Z_ne_zero {P : Fin 3 → F} (hPz : P z ≠ 0) :
W.Nonsingular P ↔ W.Equation P ∧ (eval P W.polynomialX ≠ 0 ∨ eval P W.polynomialY ≠ 0) := by
rw [nonsingular_of_Z_ne_zero hPz, Affine.Nonsingular, ← equation_of_Z_ne_zero hPz, ←
eval_polynomialX_of_Z_ne_zero hPz, div_ne_zero_iff, and_iff_left <| pow_ne_zero 2 hPz, ←
eval_polynomialY_of_Z_ne_zero hPz, div_ne_zero_iff, and_iff_left <| pow_ne_zero 2 hPz]
