aboutsummaryrefslogtreecommitdiff
path: root/src/Algebra.v
Commit message (Collapse)AuthorAge
...
* move nsatz into tactics directoryGravatar Andres Erbsen2016-06-20
|
* port CompleteEdwardsCurve.ExtendedCoordinates, make [field_algebra] try ↵Gravatar Andres Erbsen2016-06-18
| | | | fewer nonzero ports. remove FField and FNsatz
* move nsatz out of algebra, improve algebra, port CompleteEdwardsCurveTheoremsGravatar Andres Erbsen2016-06-17
|
* Z is integral domainGravatar Andres Erbsen2016-06-16
|
* algebra: add homomorphismsGravatar Andres Erbsen2016-06-16
|
* prove ring admitsGravatar Andres Erbsen2016-06-16
|
* nsatz: reimplement, integrate, demonstrateGravatar Andres Erbsen2016-06-15