corn icon indicating copy to clipboard operation
corn copied to clipboard
verified publisher icon coq-community

[math-classes] Non-commutative (semi)rings

Open urkud opened this issue 9 years ago • 2 comments

Currently MathClasses defines Ring to be a commutative ring. I propose to rename it to CommutativeRing, and introduce a Ring for non-commutative rings. Are there any objections? If no, I'll prepare a pull request.

urkud avatar Nov 30 '16 03:11 urkud

The reason we did so was because we do not have a substantial development of non-commutative rings. I'd like to wait with the change until there is a need for it. Thanks for the suggestion, though.

spitters avatar Nov 30 '16 10:11 spitters

I was going to improve the linear algebra part of math-classes. In particular, it would be nice to just say "linear maps form a ring". Actually, I think that just renaming Ring to CommutativeRing without introducing non-commutative rings is a good thing, because it improves readability for mathematicians not familiar with this library. BTW, what is the relation between Ring.v (with Ring_theory.v), Ncring.v and Cring.v in stdlib? They define rings in two different ways, and I failed to find conversion between these two versions.

urkud avatar Dec 01 '16 00:12 urkud