diff options
| author |  Andres Erbsen <andreser@mit.edu> | 2017-04-28 20:28:08 -0400 |
|---|---|---|
| committer |  GitHub <noreply@github.com> | 2017-04-28 20:28:08 -0400 |
| commit | 08be7fa27881cf4bef5bede9d07feaaa9025b9a4 (patch) | |
| tree | 18b19422c585001f784ab9066627f66940791494 /src/Algebra/Ring.v | |
| parent | e7a7d3cf71a9170ce8ce0022a7e1ae46e012b3a6 (diff) | |
Prove relationship between `xzladderstep` and M.add (#162)
* hopefully all proofs we need about xzladderstep
* Better automation in xzproofs
* Speed up xzproofs with heuristic clearing
* Remove useless hypotheses
* XZProofs cleanup
* fix "group by isomorphism" proofs, use in XZProofs
Diffstat (limited to 'src/Algebra/Ring.v')
| -rw-r--r-- | src/Algebra/Ring.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/Algebra/Ring.v b/src/Algebra/Ring.v index 406706988..2e3bcba58 100644 --- a/src/Algebra/Ring.v +++ b/src/Algebra/Ring.v @@ -205,7 +205,7 @@ Section Isomorphism. | [ H : field |- _ ] => destruct H; try clear H | [ H : commutative_ring |- _ ] => destruct H; try clear H | [ H : ring |- _ ] => destruct H; try clear H - | [ H : abelian_group |- _ ] => destruct H; try clear H + | [ H : commutative_group |- _ ] => destruct H; try clear H | [ H : group |- _ ] => destruct H; try clear H | [ H : monoid |- _ ] => destruct H; try clear H | [ H : is_commutative |- _ ] => destruct H; try clear H |