neg_of_Z_ne_zero — Mathlib

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 {R : Type r} [\text{CommRing }R],\ \forall {W : \mathrm{Jacobian}(R)},\ \forall P : \mathrm{Fin}_3 \to R,\ W.Nonsingular P \Rightarrow P_2 = 0 \Rightarrow W.neg P = -(P_1 / P_0) \cdot \![1,1,0]$$$

Lean4

theorem neg_of_Z_ne_zero {P : Fin 3 → F} (hPz : P z ≠ 0) :
    W.neg P = P z • ![P x / P z ^ 2, W.toAffine.negY (P x / P z ^ 2) (P y / P z ^ 3), 1] := by
  erw [neg, smul_fin3, mul_div_cancel₀ _ <| pow_ne_zero 2 hPz, ← negY_of_Z_ne_zero hPz,
    mul_div_cancel₀ _ <| pow_ne_zero 3 hPz, mul_one]

Похожие утверждения