addZ_of_Z_eq_zero_left

Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula

URI: https://scilib.ai/kg/mathlib#WeierstrassCurve.Jacobian.addZ_of_Z_eq_zero_left

English

If the Z-coordinate of P is zero (P_z = 0), then addZ(P,Q) reduces to P_x Q_z^2.

Русский

Если Z-координата P равна нулю (P_z = 0), то addZ(P,Q) упрощается до P_x Q_z^2.

LaTeX

$$$\text{If } P_z = 0:\quad \operatorname{addZ}(P,Q) = P_x Q_z^2$$$

Lean4

theorem addZ_of_Z_eq_zero_left {P Q : Fin 3 → R} (hPz : P z = 0) : addZ P Q = P x * Q z * Q z :=
  by
  rw [addZ, hPz]
  ring1

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

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

Разделы

Аффилиация

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