Zulip Chat Archive

Stream: new members

Topic: ring vs ring_theory


view this post on Zulip Filippo A. E. Nuccio (Sep 21 2020 at 11:50):

I have noticed that in mathlib there is both a folder ring inside algebraand a folder ring_theory in the master directory. What is the difference between the two?

view this post on Zulip Reid Barton (Sep 21 2020 at 11:58):

I don't know if there is an official answer, but my guess would be that algebra.ring contains things that are very basic and not really specific to rings, like the definition of a subring, while ring_theory is more subject-specific (that subject being mainly, at the moment, commutative algebra).

view this post on Zulip Reid Barton (Sep 21 2020 at 12:05):

That said I think we're due for some reorganization--the last time we tried to straighten things out was in Jan 2019.

view this post on Zulip Filippo A. E. Nuccio (Sep 21 2020 at 12:09):

And how does it work, by the way? I mean, there might be a lot of proofs pointing to algebra.ring, if you move the folder do the links still work?

view this post on Zulip Johan Commelin (Sep 21 2020 at 12:10):

Nope

view this post on Zulip Johan Commelin (Sep 21 2020 at 12:10):

So it's a lot of work (-;

view this post on Zulip Filippo A. E. Nuccio (Sep 21 2020 at 12:10):

I see...

view this post on Zulip Filippo A. E. Nuccio (Sep 21 2020 at 12:10):

Ok, thanks for the info, it was just out of curiosity but opened a bad Pandora box.

view this post on Zulip Scott Morrison (Sep 21 2020 at 13:31):

It's not that much work... You just have to change the relevant import statements, so searching for import algebra.ring will find most of what you need to look at.


Last updated: May 10 2021 at 00:31 UTC