aboutsummaryrefslogtreecommitdiff
path: root/src/Algebra
Commit message (Expand)AuthorAge
* make fsatz recurse when proving nonzero-ness, undo Weierstrass workaroundGravatar Andres Erbsen2017-03-30
* make 8.5 happyGravatar Andres Erbsen2017-03-02
* 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
* Weierstrass curve is a groupGravatar 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
* Fix a missing section close in ZToRingGravatar Jason Gross2017-02-10
* Accidentally pushed wrong file in last commit; this is the correct oneGravatar jadep2017-02-10
* Added ZToRing lemmasGravatar jadep2017-02-09