module
module
IndisputableMonolith.Cryptography.ECDLPWatch
show as:
view Lean formalization →
depends on (1)
declarations in this module (17)
-
structure
ShortWeierstrassCurve -
def
nonsingular -
inductive
ECPoint -
def
onCurve -
def
neg -
def
chordSlope -
def
tangentSlope -
def
slopeAddPoint -
def
pointAdd -
def
scalarMul -
inductive
CurveFamily -
structure
ECDLPInstance -
def
isSolution -
structure
PublicECDLPData -
structure
PublicInvariant -
def
isKnownWeakFamily -
structure
InvariantWatchRecord