inductive definition def or abbrev

`ECPoint`

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

formal statement (Lean)

  32inductive ECPoint (p : ℕ) where
  33  | infinity : ECPoint p
  34  | affine : ZMod p → ZMod p → ECPoint p
  35deriving DecidableEq, Repr
  36
  37/-- The curve equation, with infinity admitted as the identity point. -/

used by (7)

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

ECDLPInstance in IndisputableMonolith.Cryptography.ECDLPWatch decl_use
neg in IndisputableMonolith.Cryptography.ECDLPWatch decl_use
onCurve in IndisputableMonolith.Cryptography.ECDLPWatch decl_use
pointAdd in IndisputableMonolith.Cryptography.ECDLPWatch decl_use
PublicECDLPData in IndisputableMonolith.Cryptography.ECDLPWatch decl_use
scalarMul in IndisputableMonolith.Cryptography.ECDLPWatch decl_use
slopeAddPoint in IndisputableMonolith.Cryptography.ECDLPWatch decl_use

depends on (4)

Lean names referenced from this declaration's body.

identity in IndisputableMonolith.Foundation.ObserverForcing decl_use
as in IndisputableMonolith.Foundation.SimplicialLedger.ContinuumBridge decl_use
point in IndisputableMonolith.Numerics.Interval.Basic decl_use
identity in IndisputableMonolith.RRF.Foundation.VantageCategory decl_use