neg — Mathlib

English

There exists a natural negation operation on the projective points, turning a point into its opposite.

Русский

Существует естественное отрицание на проективных точках, переводя точку в противоположную.

LaTeX

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

Lean4

/-- The negation of a nonsingular projective point on a Weierstrass curve `W`.

Given a nonsingular projective point `P` on `W`, use `-P` instead of `neg P`. -/
def neg (P : W.Point) : W.Point :=
  ⟨nonsingularLift_negMap P.nonsingular⟩

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