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
*
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
*
Fix super_nsatz tactic to be better about ordering
Jason Gross
2016-06-28
*
Try a faster way of solving some inequalities resulting from common_denominator
Jason Gross
2016-06-27
*
Actual fix for super_nsatz
Jason Gross
2016-06-27
*
Fix super_nstaz to not error
Jason Gross
2016-06-27
*
Add a super_nsatz tactic
Jason Gross
2016-06-27
*
Fix notation level
Jason Gross
2016-06-27
*
Add global notation for eq_dec
Jason Gross
2016-06-27
*
scalarmult support; EdDSA.sign produces valid signatures
Andres Erbsen
2016-06-27
*
first pass of scalarmult
Andres Erbsen
2016-06-27
*
Add a tactic to handle "at most two square roots"
Jason Gross
2016-06-27
*
Various nsatz and field tactic improvements
Jason Gross
2016-06-24
*
Add a version of common_denominator w/o oversimpl
Jason Gross
2016-06-24
*
ExtendedCoordinates: group.
Andres Erbsen
2016-06-24
*
isomorphism_to_subgroup_group
Andres Erbsen
2016-06-24
*
Use Decidable machinery for is_eq_dec
Jason Gross
2016-06-24
*
Improve some tactics and lemmas
Jason Gross
2016-06-23
*
Add tactics to Tactics, at most 2 sq-roots to Algebra
Jason Gross
2016-06-23
[next]