pith. machine review for the scientific record. sign in
def definition def or abbrev

pointAdd

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

  66def pointAdd {p : ℕ} (E : ShortWeierstrassCurve p) : ECPoint p → ECPoint p → ECPoint p
  67  | ECPoint.infinity, Q => Q
  68  | P, ECPoint.infinity => P
  69  | ECPoint.affine x₁ y₁, ECPoint.affine x₂ y₂ =>
  70      if _hx : x₁ = x₂ then
  71        if _hy : y₁ + y₂ = 0 then
  72          ECPoint.infinity
  73        else
  74          slopeAddPoint (tangentSlope E x₁ y₁) x₁ y₁ x₁
  75      else
  76        slopeAddPoint (chordSlope x₁ y₁ x₂ y₂) x₁ y₁ x₂
  77
  78/-- Scalar multiplication by repeated addition. This is the reference
  79specification, not an efficient implementation. -/

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (10)

Lean names referenced from this declaration's body.