index
:
fiat-crypto
master
fast, formally verified cryptography
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
src
/
Algebra.v
Commit message (
Expand
)
Author
Age
*
Revert change to [nsatz] (it was making Coq run out of memory)
Jason Gross
2016-10-27
*
Various fixes in alternative nsatz
Jason Gross
2016-10-27
*
Handle folded [not] in nsatz_strip_fractions
Jason Gross
2016-10-26
*
Split inequalities before specializing
Jason Gross
2016-10-26
*
Fix nsatz: don't clear inequalities
Jason Gross
2016-10-26
*
Fix a missing case in generalize_inv
Jason Gross
2016-10-26
*
Fix typos
Jason Gross
2016-10-26
*
Add tactics to implement better fraction removal
Jason Gross
2016-10-26
*
Add lemmas about algebra
Jason Gross
2016-10-26
*
Generalize field_from_redundant_representation
Jason Gross
2016-10-23
*
Fix location of code in previous commit
Jason Gross
2016-10-17
*
Add field by isomorphism
Jason Gross
2016-10-17
*
refactor scalar multiplication thoery, implement SRepERepMul
Andres Erbsen
2016-10-12
*
Added helper lemma to Algebra.
jadep
2016-10-10
*
Add homomorphism composition
Jason Gross
2016-09-30
*
Add group and homomorphism lemmas
Jason Gross
2016-09-30
*
Weaken surjective_homomorphism_from_group
Jason Gross
2016-09-30
*
Algebra: prove an admit, add eq_r_opp_r_inv
Andres Erbsen
2016-09-16
*
Fix [ring] reference broken by moving [Require] outside a module
Jason Gross
2016-09-02
*
Silence a warning about [Require] in 8.6
Jason Gross
2016-09-02
*
Reworked square root theorems to prove they are valid iff a square root exist...
jadep
2016-08-31
*
Merge branch 'fast-inverse'
jadep
2016-08-24
|
\
*
|
remove eq_dec from Monoid
Andres Erbsen
2016-08-23
|
*
fast-inverse rebase
jadep
2016-08-22
|
/
*
address code review comments
Andres Erbsen
2016-08-04
*
Refactor ModularArithmetic into Zmod, expand Decidable
Andres Erbsen
2016-08-04
*
Move most notation level declarations into Util
Jason Gross
2016-07-27
*
Add databases for ring_simplify
Jason Gross
2016-07-22
*
Add reverse_nondep and ring_simplify_subterms_in_all tactics
Jason Gross
2016-07-22
*
Make the library 20% faster: [auto with *] is evil
Jason Gross
2016-07-22
*
Add ring_simplify_subterms
Jason Gross
2016-07-22
*
proved an admit in field homomorphisms that turned out to be unprovable; I ad...
jadep
2016-07-15
*
cleaned Specific operations so they produce code without proof terms, and pro...
jadep
2016-07-12
*
prove that if something is isomorphic to a field, it is a field
jadep
2016-07-11
*
s/conservative_common_denominator/common_denominator/g
Andres Erbsen
2016-07-11
*
rename [common_denominator] to [field_simplify_if_div]
Andres Erbsen
2016-07-11
*
remove field_algebra
Andres Erbsen
2016-07-11
*
wrap nsatz in Algebra
Andres Erbsen
2016-07-11
*
added proofs about addition chain exponentiation for later use in ModularBase...
jadep
2016-07-10
*
super_nsatz: Handle x^2 = y^2 -> x <> -y -> x = y
Jason Gross
2016-07-02
*
Simplify conservative_common_denominator
Jason Gross
2016-06-29
*
Don't generate goals [False] in conservative_common_denominator_all
Jason Gross
2016-06-29
*
Fix [only_two_square_roots] to not loop
Jason Gross
2016-06-29
*
Allow side-conditions in common denom. all in hyps
Jason Gross
2016-06-29
*
Handle fractions in denominators
Jason Gross
2016-06-29
*
Clear symmetric duplicates in clear_algebraic_duplicates
Jason Gross
2016-06-29
*
Fix a typo in the previous commit
Jason Gross
2016-06-28
*
[super_nstaz]: Handle side-conditions from [nsatz]
Jason Gross
2016-06-28
*
No more anomalies from super_nsatz, hopefully
Jason Gross
2016-06-28
*
Fix a typo (missing .)
Jason Gross
2016-06-28
[next]