instAdd

Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point

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

English

There is a noncomputable instance providing the addition operation on W.Point, i.e., an Add structure is available.

Русский

Существует невычислимый экземпляр, предоставляющий операцию сложения на W.Point, то есть имеется структура Add.

LaTeX

$$instance : Add W.Point$$

Lean4

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

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

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

Разделы

Аффилиация

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