add_self

Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point

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

English

For any P, the sum of P with itself equals the doubling of P: W'.add P P = W'.dblXYZ P.

Русский

Для любой P сумма P с самим собой равна удвоению P: W'.add P P = W'.dblXYZ P.

LaTeX

$$$ W'.add P P = W'.dblXYZ P $$$

Lean4

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

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

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

Разделы

Аффилиация

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