aboutsummaryrefslogtreecommitdiff
path: root/src/Algebra.v
Commit message (Expand)AuthorAge
* rename-everythingGravatar Andres Erbsen2017-04-06
* make elliptic curve proofs faster and split them into filesGravatar Andres Erbsen2017-04-05
* Add [Proof using] to most proofsGravatar Jason Gross2017-04-04
* More fine-grained tactic importsGravatar Jason Gross2017-04-03
* use [positive] for [F] modulus, char_ge_C instead of char_gt_CGravatar Andres Erbsen2017-03-02
* address some code review commentsGravatar Andres Erbsen2017-03-02
* split the algebra library; use fsatz moreGravatar Andres Erbsen2017-03-02
* fsatz, nsatz_solve_nonzeroGravatar Andres Erbsen2017-03-02
* field_nsatzGravatar Andres Erbsen2017-03-02
* field_nsatzGravatar Andres Erbsen2017-02-06
* 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-17 08:21:29 +0000