diff options
| author |  Andres Erbsen <andreser@mit.edu> | 2017-02-15 13:18:40 -0500 |
|---|---|---|
| committer | Andres Erbsen <andreser@mit.edu> | 2017-03-02 13:37:14 -0500 |
| commit | 0a6e65e3cec0a8f00f357d82489532203f315389 (patch) | |
| tree | b7bc706ce46b38e3c43f9375fd5a2dd9859d056a /src/Algebra/Ring.v | |
| parent | 0a9ea9df752b078bbd89f765cf760081036bd51a (diff) | |
address some code review comments
Diffstat (limited to 'src/Algebra/Ring.v')
| -rw-r--r-- | src/Algebra/Ring.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/src/Algebra/Ring.v b/src/Algebra/Ring.v index 3752c7562..b69e9b191 100644 --- a/src/Algebra/Ring.v +++ b/src/Algebra/Ring.v @@ -46,7 +46,7 @@ Section Ring. rewrite <-!associative, right_inverse, right_identity; reflexivity. Qed. - Definition opp_nonzero_nonzero : forall x, x <> 0 -> opp x <> 0 := Group.inv_nonzero_nonzero. + Definition opp_zero_iff : forall x, opp x = 0 <-> x = 0 := Group.inv_id_iff. Global Instance is_left_distributive_sub : is_left_distributive (eq:=eq)(add:=sub)(mul:=mul). Proof. @@ -360,7 +360,7 @@ End of_Z. Definition char_gt {R eq zero one opp add} {sub:R->R->R} {mul:R->R->R} C := - @Algebra.char_gt R eq zero (fun n => (@of_Z R zero one opp add) (BinInt.Z.of_N n)) C. + @Algebra.char_gt R eq zero (fun p => (@of_Z R zero one opp add) (BinInt.Z.pos p)) C. Existing Class char_gt. (*** Tactics for ring equations *) |