add_of_equiv

Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point

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

English

If P ≈ Q, then add(P,Q) = dblXYZ(P).

Русский

Если P ≈ Q, тогда add(P,Q) = dblXYZ(P).

LaTeX

$$$P \approx Q \Rightarrow \mathrm{add}(P,Q) = \mathrm{dblXYZ}(P)$$$

Lean4

theorem add_of_equiv {P Q : Fin 3 → R} (h : P ≈ Q) : W'.add P Q = W'.dblXYZ P :=
  if_pos h

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

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

Разделы

Аффилиация

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