negY_of_Z_ne_zero — Mathlib

English

If P_z ≠ 0, then the ratio W'.negY P over P_z equals the affine Y-coordinate of the affine point (P_x/P_z, P_y/P_z).

Русский

Если P_z ≠ 0, то отношение W'.negY P к P_z равно аффинной Y-координате точки (P_x/P_z, P_y/P_z).

LaTeX

$$$ \\frac{W'.negY P}{P_z} = W'.toAffine.negY\\left(\\frac{P_x}{P_z}, \\frac{P_y}{P_z}\\right) $$$

Lean4

theorem negY_of_Z_ne_zero {P : Fin 3 → F} (hPz : P z ≠ 0) : W.negY P / P z = W.toAffine.negY (P x / P z) (P y / P z) :=
  by linear_combination (norm := (rw [negY, Affine.negY]; ring1)) -W.a₃ * div_self hPz

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