addX_neg

Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point

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

English

The X-coordinate of P + (neg P) is zero: addX P (neg P) = 0.

Русский

Координата X суммы P и (−P) равна нулю.

LaTeX

$$$$\mathrm{addX}(P, \mathrm{neg} P) = 0$$$$

Lean4

theorem addX_neg (P : Fin 3 → R) : W'.addX P (W'.neg P) = 0 :=
  by
  rw [addX, neg_X, neg_Y, neg_Z, negY]
  ring1

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

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

Разделы

Аффилиация

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