instAdd

Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point

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

English

Addition of two projective points satisfies the usual law: P + Q equals the result of the defined addition operation, namely P.add Q.

Русский

Сложение двух проективных точек удовлетворяет обычному закону: P + Q равно результату операции сложения, то есть P.add Q.

LaTeX

$$$ P + Q = P.add Q $$$

Lean4

noncomputable instance : Add W.Point :=
  ⟨add⟩

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

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

Разделы

Аффилиация

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