aboutsummaryrefslogtreecommitdiff
path: root/src/Algebra/Ring.v
Commit message (Expand)AuthorAge
* Make trivial instances explicitGravatar Maxime Dénès2019-01-24
* Don't rely on autogenerated namesGravatar Jason Gross2017-06-05
* Prove relationship between `xzladderstep` and M.add (#162)Gravatar Andres Erbsen2017-04-28
* rename-everythingGravatar Andres Erbsen2017-04-06
* Add [Proof using] to most proofsGravatar Jason Gross2017-04-04
* More fine-grained tactic importsGravatar Jason Gross2017-04-03
* PrimeFieldTheorems: inv for isomorphic fieldsGravatar Andres Erbsen2017-03-02
* use [positive] for [F] modulus, char_ge_C instead of char_gt_CGravatar Andres Erbsen2017-03-02
* rewrite ExtendedCoordinates, fix Ed25519Gravatar Andres Erbsen2017-03-02
* address some code review commentsGravatar Andres Erbsen2017-03-02
* change weierstrass spec, prove most cases of associativityGravatar Andres Erbsen2017-03-02
* split the algebra library; use fsatz moreGravatar Andres Erbsen2017-03-02