addZ_neg

Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point

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

English

The quantity addZ of a point P with its negation is identically zero: addZ P (neg P) = 0.

Русский

Сумма addZ точки P и её отрицания равна нулю: addZ P (neg P) = 0.

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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