aboutsummaryrefslogtreecommitdiff
path: root/src/WeierstrassCurve
Commit message (Expand)AuthorAge
* use improved fsatz on various elliptic curve thingsGravatar Andres Erbsen2017-03-31
* make fsatz recurse when proving nonzero-ness, undo Weierstrass workaroundGravatar Andres Erbsen2017-03-30
* use [positive] for [F] modulus, char_ge_C instead of char_gt_CGravatar Andres Erbsen2017-03-02
* WIPGravatar Andres Erbsen2017-03-02
* address some code review commentsGravatar Andres Erbsen2017-03-02
* Weierstrass curve is a groupGravatar Andres Erbsen2017-03-02
* Attempt Weierstrass associativity again, good progress.Gravatar Andres Erbsen2017-03-02
* split the algebra library; use fsatz moreGravatar Andres Erbsen2017-03-02
* remove eq_dec from MonoidGravatar Andres Erbsen2016-08-23
* Refactor ModularArithmetic into Zmod, expand DecidableGravatar Andres Erbsen2016-08-04
* Move most notation level declarations into UtilGravatar Jason Gross2016-07-27
* remove field_algebraGravatar Andres Erbsen2016-07-11
* port CompleteEdwardsCurveTheorems (builds again)Gravatar Andres Erbsen2016-07-11
* Define the spec of Weierstrass curves (#6)Gravatar Jason Gross2016-07-03