aboutsummaryrefslogtreecommitdiff
path: root/src/Algebra.v
Commit message (Expand)AuthorAge
* Move most notation level declarations into UtilGravatar Jason Gross2016-07-27
* Add databases for ring_simplifyGravatar Jason Gross2016-07-22
* Add reverse_nondep and ring_simplify_subterms_in_all tacticsGravatar Jason Gross2016-07-22
* Make the library 20% faster: [auto with *] is evilGravatar Jason Gross2016-07-22
* Add ring_simplify_subtermsGravatar Jason Gross2016-07-22
* proved an admit in field homomorphisms that turned out to be unprovable; I ad...Gravatar jadep2016-07-15
* cleaned Specific operations so they produce code without proof terms, and pro...Gravatar jadep2016-07-12
* prove that if something is isomorphic to a field, it is a fieldGravatar jadep2016-07-11
* s/conservative_common_denominator/common_denominator/gGravatar Andres Erbsen2016-07-11
* rename [common_denominator] to [field_simplify_if_div]Gravatar Andres Erbsen2016-07-11
* remove field_algebraGravatar Andres Erbsen2016-07-11
* wrap nsatz in AlgebraGravatar Andres Erbsen2016-07-11
* added proofs about addition chain exponentiation for later use in ModularBase...Gravatar jadep2016-07-10
* super_nsatz: Handle x^2 = y^2 -> x <> -y -> x = yGravatar Jason Gross2016-07-02
* Simplify conservative_common_denominatorGravatar Jason Gross2016-06-29
* Don't generate goals [False] in conservative_common_denominator_allGravatar Jason Gross2016-06-29
* Fix [only_two_square_roots] to not loopGravatar Jason Gross2016-06-29
* Allow side-conditions in common denom. all in hypsGravatar Jason Gross2016-06-29
* Handle fractions in denominatorsGravatar Jason Gross2016-06-29
* Clear symmetric duplicates in clear_algebraic_duplicatesGravatar Jason Gross2016-06-29
* Fix a typo in the previous commitGravatar Jason Gross2016-06-28
* [super_nstaz]: Handle side-conditions from [nsatz]Gravatar Jason Gross2016-06-28
* No more anomalies from super_nsatz, hopefullyGravatar Jason Gross2016-06-28
* 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-03 01:41:22 +0000