add_of_eq

Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point

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

English

If P ≉ Q, then add(P,Q) = addXYZ(P,Q).

Русский

Если P не эквивалентна Q, то add(P,Q) = addXYZ(P,Q).

LaTeX

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

Lean4

theorem add_of_eq {P Q : Fin 3 → R} (h : P = Q) : W'.add P Q = W'.dblXYZ P :=
  h ▸ add_self P

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

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

Разделы

Аффилиация

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