instAddCommGroup — Mathlib

English

The affine Weierstrass points form an abelian group under the standard point addition law coming from the elliptic curve.

Русский

Точки аффинной кривой Вейерштрасса образуют абелеву группу под обычной операцией сложения точек на эллиптической кривой.

LaTeX

$$$W.Point \text{ with the Weierstrass addition is an abelian group}$$$

Lean4

instance : AddCommGroup W.Point where
  nsmul := nsmulRec
  zsmul := zsmulRec
  zero_add := zero_add
  add_zero := add_zero
  neg_add_cancel _ := by rw [add_eq_zero]
  add_comm _ _ := toClass_injective <| by simp only [map_add, add_comm]
  add_assoc _ _ _ := toClass_injective <| by simp only [map_add, add_assoc]

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