addXYZ_of_Z_eq_zero_left — Mathlib

English

If hP is a Weierstrass point and P z = 0, then addXYZ(P,Q) = (P_y^2 Q_z) · Q.

Русский

Если P — точка на кривой и P z = 0, то addXYZ(P,Q) = (P_y^2 Q_z) · Q.

LaTeX

$$$\mathrm{addXYZ}(P,Q) = (P_y^2 \cdot Q_z) \cdot Q$$$

Lean4

theorem addXYZ_of_Z_eq_zero_left [NoZeroDivisors R] {P Q : Fin 3 → R} (hP : W'.Equation P) (hPz : P z = 0) :
    W'.addXYZ P Q = (P y ^ 2 * Q z) • Q := by
  rw [addXYZ, addX_of_Z_eq_zero_left hP hPz, addY_of_Z_eq_zero_left hP hPz, addZ_of_Z_eq_zero_left hP hPz, smul_fin3]

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