neg_def

Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point

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

English

See previous neg_point: the negation of a point corresponds to negation of its underlying representation.

Русский

См. предыдущий neg_point: отрицание точки соответствует отрицанию её базового представления.

LaTeX

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

Lean4

theorem neg_def (P : W.Point) : -P = P.neg :=
  rfl

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

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

Разделы

Аффилиация

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