aboutsummaryrefslogtreecommitdiff
path: root/src/Algebra
Commit message (Expand)AuthorAge
* Make trivial instances explicitGravatar Maxime Dénès2019-01-24
* Import prim token notations before using themGravatar Jason Gross2018-08-24
* subsetoid_ring: don't ask for false thingsGravatar Jason Gross2018-03-12
* Add Algebra.SubsetoidRingGravatar Jason Gross2018-03-12
* fsatz tests: 1/(1/x) = xGravatar Andres Erbsen2017-09-11
* ScalarMult: Z -> G -> G (closes #193)Gravatar Andres Erbsen2017-06-14
* Don't rely on autogenerated namesGravatar Jason Gross2017-06-05
* Strip trailing whitespaceGravatar Jason Gross2017-06-02
* Prove relationship between `xzladderstep` and M.add (#162)Gravatar Andres Erbsen2017-04-28
* clean elliptic curve proofs, use par: in WeierstrassAffineProofsGravatar 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
* 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-02 01:17:31 +0000