diff options
Diffstat (limited to 'src/Algebra/Ring.v')
| -rw-r--r-- | src/Algebra/Ring.v | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/src/Algebra/Ring.v b/src/Algebra/Ring.v index f39d730f2..640b12ed9 100644 --- a/src/Algebra/Ring.v +++ b/src/Algebra/Ring.v @@ -388,11 +388,11 @@ Section of_Z. Qed. End of_Z. -Definition char_gt +Definition char_ge {R eq zero one opp add} {sub:R->R->R} {mul:R->R->R} 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. + @Algebra.char_ge R eq zero (fun p => (@of_Z R zero one opp add) (BinInt.Z.pos p)) C. +Existing Class char_ge. (*** Tactics for ring equations *) Require Export Coq.setoid_ring.Ring_tac. |