add — Mathlib

English

There is a natural addition operation on projective points making the triple (W, P, Q) into an additive structure.

Русский

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

LaTeX

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

Lean4

/-- The addition of two nonsingular projective points on a Weierstrass curve `W`.

Given two nonsingular projective points `P` and `Q` on `W`, use `P + Q` instead of `add P Q`. -/
noncomputable def add (P Q : W.Point) : W.Point :=
  ⟨nonsingularLift_addMap P.nonsingular Q.nonsingular⟩

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