addX_self — Mathlib

English

Under the curve equations, addX satisfies a cross-multiplied relation: addX(P,Q)·(Pz Qz)^2 equals a specific polynomial times (Px Qz − Qx Pz).

Русский

При условиях уравнений кривой addX удовлетворяет отношению после перемножения: addX(P,Q)·(Pz Qz)^2 равно полиному, умноженному на (Px Qz − Qx Pz).

LaTeX

$$$W'.addX(P,Q) \cdot (P_z Q_z)^2 = \, \big( (P_y Q_z - Q_y P_z)^2 P_z Q_z + a_1 (P_y Q_z - Q_y P_z) P_z Q_z (P_x Q_z - Q_x P_z) \, - a_2 P_z Q_z (P_x Q_z - Q_x P_z)^2 - P_x Q_z (P_x Q_z - Q_x P_z)^2 - Q_x P_z (P_x Q_z - Q_x P_z)^2 \big) (P_x Q_z - Q_x P_z).$$

Lean4

theorem addX_self (P : Fin 3 → R) : W'.addX P P = 0 := by
  rw [addX]
  ring1

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