English
If P is nonsingular and P_2 = 0, then W.neg P equals - (P_1 / P_0) times [1,1,0].
Русский
Если P несингулярна и P_2 = 0, то W.neg P равно - (P_1 / P_0) умноженное на [1,1,0].
LaTeX
$$$\forall {F : Type},\ [\text{Field }F],\ \forall {W : \mathrm{Jacobian}(F)},\ \forall P : \mathrm{Fin}_3 \to F,\ W.Nonsingular P \Rightarrow P_2 = 0 \Rightarrow W.\neg P = -\frac{P_1}{P_0} \cdot \![1,1,0]$$$
Lean4
theorem neg_of_Z_eq_zero {P : Fin 3 → F} (hP : W.Nonsingular P) (hPz : P z = 0) : W.neg P = -(P y / P x) • ![1, 1, 0] :=
by
have hX {n : ℕ} : IsUnit <| P x ^ n := (isUnit_X_of_Z_eq_zero hP hPz).pow n
erw [neg_of_Z_eq_zero' hPz, smul_fin3, neg_sq, div_pow, (equation_of_Z_eq_zero hPz).mp hP.left, pow_succ,
hX.mul_div_cancel_left, mul_one, Odd.neg_pow <| by decide, div_pow, pow_succ,
(equation_of_Z_eq_zero hPz).mp hP.left, hX.mul_div_cancel_left, mul_one, mul_zero]
