neg_def

Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point

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

English

Negation operation is formally an instance on the point type of the Weierstrass projective curve.

Русский

Отрицание формально задается как экземпляр на типе точек кривой Ваерштрасса.

LaTeX

$$$\text{instance } : \text{Neg } W.Point$$$

Lean4

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

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

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

Разделы

Аффилиация

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