inductive definition def or abbrev

`CurveFamily`

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

formal statement (Lean)

  85inductive CurveFamily where
  86  | toy
  87  | anomalous
  88  | supersingular
  89  | smallEmbeddingDegree
  90  | ordinaryPrimeOrder
  91  | standardLike
  92deriving DecidableEq, Repr
  93
  94/-- Minimal ECDLP instance: recover `k` from `Q = kP`. -/

used by (4)

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

ECDLPInstance in IndisputableMonolith.Cryptography.ECDLPWatch decl_use
InvariantWatchRecord in IndisputableMonolith.Cryptography.ECDLPWatch decl_use
isKnownWeakFamily in IndisputableMonolith.Cryptography.ECDLPWatch decl_use
PublicECDLPData in IndisputableMonolith.Cryptography.ECDLPWatch decl_use

depends on (1)

Lean names referenced from this declaration's body.

from in IndisputableMonolith.Foundation.PrimitiveDistinction decl_use