instAdd

Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point

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

English

Provide a canonical additive structure on the Weierstrass affine curve points via an instance of the Add typeclass.

Русский

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

LaTeX

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

Lean4

instance : Add W.Point :=
  ⟨add⟩

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

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

Разделы

Аффилиация

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