search

coq-community / corn

Coq Repository at Nijmegen [maintainers=@spitters,@VincentSe,@Lysxia]
http://c-corn.github.io/
GNU General Public License v2.0
108 stars 43 forks source link

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

Open urkud opened 7 years ago

urkud commented 7 years ago

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.

spitters commented 7 years ago

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.

urkud commented 7 years ago

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.