aboutsummaryrefslogtreecommitdiff
path: root/src/Arithmetic/Karatsuba.v
diff options
context:
space:
mode:
authorGravatar Andres Erbsen <andreser@mit.edu>2017-04-28 20:28:08 -0400
committerGravatar GitHub <noreply@github.com>2017-04-28 20:28:08 -0400
commit08be7fa27881cf4bef5bede9d07feaaa9025b9a4 (patch)
tree18b19422c585001f784ab9066627f66940791494 /src/Arithmetic/Karatsuba.v
parente7a7d3cf71a9170ce8ce0022a7e1ae46e012b3a6 (diff)
Prove relationship between `xzladderstep` and M.add (#162)
* hopefully all proofs we need about xzladderstep * Better automation in xzproofs * Speed up xzproofs with heuristic clearing * Remove useless hypotheses * XZProofs cleanup * fix "group by isomorphism" proofs, use in XZProofs
Diffstat (limited to 'src/Arithmetic/Karatsuba.v')
0 files changed, 0 insertions, 0 deletions