add_self

Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point

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

English

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

Русский

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

LaTeX

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

Lean4

theorem add_self (P : Fin 3 → R) : W'.add P P = W'.dblXYZ P :=
  add_of_equiv <| Setoid.refl _

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

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

Разделы

Аффилиация

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