Separating `NNRat` casts from `Data.Rat.Cast`

Stream: mathlib4

[Peter Hansen]

As I'm new to contributing, I'm trying to better understand the library's structure and had a question about the Data.Rat.Cast directory.

I noticed that the files in this directory contain theorems for cast for both Rat (into division rings) and NNRat (into division semirings). I was wondering if it would make sense to create a new, parallel directory Data.NNRat.Cast? This would create a dedicated and discoverable home for all the results about NNRat casts, while allowing Data.Rat.Cast to be focused solely on Rat.

Is this a sensible refactor, or is there a reason for the current mixed structure that I might be overlooking?

[Ruben Van de Velde]

@Yaël Dillies do you have thoughts?

[Yaël Dillies]

Peter is coming from #26480, where I had thoughts :wink:

[Yaël Dillies]

To avoid people digging through the conversations: No, that's a bad idea. A much better idea would be to move all this Cast content to the Algebra.Field and Algebra.Order.Field folders, and one file in each should be enough

[Peter Hansen]

Yaël Dillies said:

Peter is coming from #26480, where I had thoughts

Oh, I did not mean to ignore the advice you gave in #26480. I just thought that it only pertained to ℚ≥0 → WithTop K.

[Yaël Dillies]

Aha, no, my advice is the same for both situations