def definition def or abbrev

`scalarMul`

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

formal statement (Lean)

  80def scalarMul {p : ℕ} (E : ShortWeierstrassCurve p) : ℕ → ECPoint p → ECPoint p
  81  | 0, _P => ECPoint.infinity
  82  | n + 1, P => pointAdd E P (scalarMul E n P)
  83
  84/-- Curve-family tag used by the watch harness. -/

used by (2)

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

isSolution in IndisputableMonolith.Cryptography.ECDLPWatch decl_use
LinearAlgebraOp in IndisputableMonolith.Mathematics.LinearAlgebraFromRS decl_use

depends on (4)

Lean names referenced from this declaration's body.

ECPoint in IndisputableMonolith.Cryptography.ECDLPWatch decl_use
pointAdd in IndisputableMonolith.Cryptography.ECDLPWatch decl_use
ShortWeierstrassCurve in IndisputableMonolith.Cryptography.ECDLPWatch decl_use
E in IndisputableMonolith.Foundation.SpectralEmergence decl_use