ring vs ring_theory

Stream: new members

[Filippo A. E. Nuccio]

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?

[Reid Barton]

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).

[Reid Barton]

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

[Filippo A. E. Nuccio]

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?

[Johan Commelin]

Nope

[Johan Commelin]

So it's a lot of work (-;

[Filippo A. E. Nuccio]

I see...

[Filippo A. E. Nuccio]

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

[Scott Morrison]

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.