addX_of_Z_eq_zero_right

Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula

URI: https://scilib.ai/kg/mathlib#WeierstrassCurve.Projective.addX_of_Z_eq_zero_right

← MathLib Explorer

English

If Q lies on the curve with Q_z = 0, then X(P,Q) = −(Q_y^2 P_z) P_x.

Русский

Если Qz = 0, то X(P,Q) = −(Q_y^2 P_z) P_x.

LaTeX

$$$W'.addX(P,Q) = -(Q_y^2 \cdot P_z) \cdot P_x$, при $Q_z = 0$.$$

Lean4

theorem addX_of_Z_eq_zero_right [NoZeroDivisors R] {P Q : Fin 3 → R} (hQ : W'.Equation Q) (hQz : Q z = 0) :
    W'.addX P Q = -(Q y ^ 2 * P z) * P x :=
  by
  rw [addX, hQz, X_eq_zero_of_Z_eq_zero hQ hQz]
  ring1

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru