instNeg

Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point

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

English

For any point P, the negation defined by the structure coincides with the negation map applied to P.

Русский

Для любой точки P её отрицание по структуре совпадает с применением к P отображения минуса.

LaTeX

$$$ (-P) = P.neg $$$

Lean4

instance : Neg W.Point :=
  ⟨neg⟩

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

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

Разделы

Аффилиация

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