English
The nonsingularity condition, defined as W'.Nonsingular P, is equivalent to the conjunction of W'.Equation P with a nonzero condition on at least one of the derivatives W'.polynomialX, W'.polynomialY, W'.polynomialZ, i.e., at least one of these derivatives evaluated at P is nonzero.
Русский
Условие невырожденности, определяемое как W'.Nonsingular P, эквивалентно сочетанию W'.Equation P и того, что не все частные производные обнуляются: по меньшей мере одна из W'.polynomialX, W'.polynomialY, W'.polynomialZ не равна нулю в P.
LaTeX
$$$W'.Nonsingular P \\iff (W'.Equation P) \\land (W'.a_1 P_y P_z - (3 P_x^2 + 2 W'.a_2 P_x P_z + W'.a_4 P_z^2) \\neq 0 \\lor 2 P_y P_z + W'.a_1 P_x P_z + W'.a_3 P_z^2 \\neq 0 \\lor P_y^2 + W'.a_1 P_x P_y + 2 W'.a_3 P_y P_z - (W'.a_2 P_x^2 + 2 W'.a_4 P_x P_z + 3 W'.a_6 P_z^2) \\neq 0)$$$
Lean4
theorem polynomialZ_eq :
W'.polynomialZ =
Y ^ 2 + C W'.a₁ * X * Y + C (2 * W'.a₃) * Y * Z -
(C W'.a₂ * X ^ 2 + C (2 * W'.a₄) * X * Z + C (3 * W'.a₆) * Z ^ 2) :=
by
rw [polynomialZ, polynomial]
pderiv_simp
ring1
