aboutsummaryrefslogtreecommitdiff
path: root/src/Algebra.v
Commit message (Expand)AuthorAge
...
* Fix a typo (missing .)Gravatar Jason Gross2016-06-28
* Fix super_nsatz tactic to be better about orderingGravatar Jason Gross2016-06-28
* Try a faster way of solving some inequalities resulting from common_denominatorGravatar Jason Gross2016-06-27
* Actual fix for super_nsatzGravatar Jason Gross2016-06-27
* Fix super_nstaz to not errorGravatar Jason Gross2016-06-27
* Add a super_nsatz tacticGravatar Jason Gross2016-06-27
* Fix notation levelGravatar Jason Gross2016-06-27
* Add global notation for eq_decGravatar Jason Gross2016-06-27
* scalarmult support; EdDSA.sign produces valid signaturesGravatar Andres Erbsen2016-06-27
* first pass of scalarmultGravatar Andres Erbsen2016-06-27
* Add a tactic to handle "at most two square roots"Gravatar Jason Gross2016-06-27
* Various nsatz and field tactic improvementsGravatar Jason Gross2016-06-24
* Add a version of common_denominator w/o oversimplGravatar Jason Gross2016-06-24
* ExtendedCoordinates: group.Gravatar Andres Erbsen2016-06-24
* isomorphism_to_subgroup_groupGravatar Andres Erbsen2016-06-24
* Use Decidable machinery for is_eq_decGravatar Jason Gross2016-06-24
* 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-01 00:38:57 +0000