aboutsummaryrefslogtreecommitdiff
path: root/src/Algebra.v
Commit message (Expand)AuthorAge
* Improve some tactics and lemmasGravatar Jason Gross2016-06-23
* Add tactics to Tactics, at most 2 sq-roots to AlgebraGravatar Jason Gross2016-06-23
* surjective homomorphism from group makes a groupGravatar Andres Erbsen2016-06-23
* Make [nsatz_contradict] better at inequalitiesGravatar Jason Gross2016-06-23
* [field_algebra] now knows that 0 <> -0 is falseGravatar Jason Gross2016-06-23
* Add tactics for canonicalizing field (in)equalitiesGravatar Jason Gross2016-06-23
* Rename the nonzero lemma to an iff lemmaGravatar Jason Gross2016-06-23
* Add mul_nonzero_nonzero_and to Algebra.vGravatar Jason Gross2016-06-23
* Algebra: change a aliasing definition into an aliasing lemma to appease impli...Gravatar Andres Erbsen2016-06-20
* More missing scopes for 8.5?Gravatar Jason Gross2016-06-20
* Fix for Coq 8.4pl2Gravatar Jason Gross2016-06-20
* move nsatz into tactics directoryGravatar Andres Erbsen2016-06-20
* port CompleteEdwardsCurve.ExtendedCoordinates, make [field_algebra] try fewer...Gravatar Andres Erbsen2016-06-18
* 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-19 21:13:14 +0000