neg_point

Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point

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

English

The coordinates of the negation of a point are given by the negation map applied to the coordinates of the point.

Русский

Координаты отрицания точки задаются применением отображения минуса к координатам точки.

LaTeX

$$$ (-P).point = W.negMap P.point $$$

Lean4

theorem neg_point (P : W.Point) : (-P).point = W.negMap P.point :=
  rfl

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

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

Разделы

Аффилиация

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