The Coq mailing list

[Vadim Zaliva <vzaliva AT cmu.edu>]

I have noticed that Semiring definition: 

https://github.com/coq/coq/blob/trunk/plugins/setoid_ring/Ring_theory.v

defines multiplication as commutative. It most definitions I’ve seen it is 
usually
non-commutative:

[1] http://mathworld.wolfram.com/Semiring.html
[2] 
https://github.com/math-classes/math-classes/blob/master/interfaces/abstract_algebra.v

Was it intentional or just an error?

P.S. The problem propagates up to MathClasses which are following the same 
definition as in Coq
standard library.

Sincerely,
Vadim Zaliva

--
CMU ECE PhD student
Mobile: +1(510)220-1060
Skype: vzaliva