addY_self

Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula

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

← MathLib Explorer

English

If P_z = 0, then addY(P,Q) reduces to P_y^2 Q_z Q_y.

Русский

Если P_z = 0, то addY(P,Q) упрощается до P_y^2 Q_z Q_y.

LaTeX

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

Lean4

theorem addY_self (P : Fin 3 → R) : W'.addY P P = 0 := by
  simp only [addY, negY_eq, negAddY_self, addX_self, addZ_self, neg_zero, mul_zero, sub_zero]

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

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

Разделы

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

Аффилиация

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