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
*
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
*
surjective homomorphism from group makes a group
Andres Erbsen
2016-06-23
*
Make [nsatz_contradict] better at inequalities
Jason Gross
2016-06-23
*
[field_algebra] now knows that 0 <> -0 is false
Jason Gross
2016-06-23
*
Add tactics for canonicalizing field (in)equalities
Jason Gross
2016-06-23
*
Rename the nonzero lemma to an iff lemma
Jason Gross
2016-06-23
*
Add mul_nonzero_nonzero_and to Algebra.v
Jason Gross
2016-06-23
*
Algebra: change a aliasing definition into an aliasing lemma to appease impli...
Andres Erbsen
2016-06-20
*
More missing scopes for 8.5?
Jason Gross
2016-06-20
[next]