aboutsummaryrefslogtreecommitdiff
path: root/src/ModularArithmetic/Montgomery/ZProofs.v
Commit message (Expand)AuthorAge
* 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
* Work around broken lia in 8.4Gravatar Jason Gross2016-08-09
* Add alternate form of Montgomery, which does better about boundsGravatar Jason Gross2016-08-09
* Montgomery: Add a variant that does reduction through partial_reduceGravatar Jason Gross2016-08-08
* Define Montgomery reduction / multiplication on Z (#42)Gravatar Jason Gross2016-08-05