instAddZeroClass

Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point

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

English

There is a zero element for addition on W.Point making it an AddZeroClass.

Русский

Существует ноль для сложения на W.Point, делая его AddZeroClass.

LaTeX

$$$\\text{instance }\\text{ AddZeroClass } W.Point$$$

Lean4

instance : AddZeroClass W.Point where
  zero_add := by rintro (_ | _) <;> rfl
  add_zero := by rintro (_ | _) <;> rfl

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

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

Разделы

Аффилиация

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