aboutsummaryrefslogtreecommitdiff
path: root/src/Algebra.v
Commit message (Expand)AuthorAge
* Added new algebra lemmaGravatar jadep2016-10-30
* Revert change to [nsatz] (it was making Coq run out of memory)Gravatar Jason Gross2016-10-27
* Various fixes in alternative nsatzGravatar Jason Gross2016-10-27
* Handle folded [not] in nsatz_strip_fractionsGravatar Jason Gross2016-10-26
* Split inequalities before specializingGravatar Jason Gross2016-10-26
* Fix nsatz: don't clear inequalitiesGravatar Jason Gross2016-10-26
* Fix a missing case in generalize_invGravatar Jason Gross2016-10-26
* Fix typosGravatar Jason Gross2016-10-26
* Add tactics to implement better fraction removalGravatar Jason Gross2016-10-26
* Add lemmas about algebraGravatar Jason Gross2016-10-26
* Generalize field_from_redundant_representationGravatar Jason Gross2016-10-23
* Fix location of code in previous commitGravatar Jason Gross2016-10-17
* Add field by isomorphismGravatar Jason Gross2016-10-17
* refactor scalar multiplication thoery, implement SRepERepMulGravatar Andres Erbsen2016-10-12
* Added helper lemma to Algebra.Gravatar jadep2016-10-10
* Add homomorphism compositionGravatar Jason Gross2016-09-30
* Add group and homomorphism lemmasGravatar Jason Gross2016-09-30
* Weaken surjective_homomorphism_from_groupGravatar Jason Gross2016-09-30
* Algebra: prove an admit, add eq_r_opp_r_invGravatar Andres Erbsen2016-09-16
* Fix [ring] reference broken by moving [Require] outside a moduleGravatar Jason Gross2016-09-02
* Silence a warning about [Require] in 8.6Gravatar Jason Gross2016-09-02
* Reworked square root theorems to prove they are valid iff a square root exist...Gravatar jadep2016-08-31
* Merge branch 'fast-inverse'Gravatar jadep2016-08-24
|\
* | remove eq_dec from MonoidGravatar Andres Erbsen2016-08-23
| * fast-inverse rebaseGravatar jadep2016-08-22
|/
* address code review commentsGravatar Andres Erbsen2016-08-04
* Refactor ModularArithmetic into Zmod, expand DecidableGravatar Andres Erbsen2016-08-04
* 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-16 03:44:34 +0000