Remove `ext` attribute to `Rat`

Stream: batteries

[Damiano Testa]

Following this discussion, I would like to remove the ext attribute to Rat.

However, I never made a PR to Std: do I need push access to make a PR? If so, could I have it? Otherwise, what am I supposed to do? Thanks!

[Eric Rodriguez]

You're meant to fork Std, I think

[Damiano Testa]

I hope I did everything correctly: std#611.

I do not know how to check if mathlib still builds, though...

[Kim Morrison]

You can open lakefile.lean in Mathlib, and change the require line for Std from main to the name of your branch. Then run lake build and see what happens!

[Kim Morrison]

(This assumes that Mathlib can actually cope with the latest Std; but usually I bump it at least every few days.)

[Jireh Loreaux]

@Mario Carneiro and @Joe Hendrix : Is Std amenable to scoping Rat.ext to the Rat namespace? (Is that even possible right now? I suspect Mathlib might still have the scoping code; in that case I'm asking about moving both things.)

[Jireh Loreaux]

Sorry, I just saw this thread

[Notification Bot]

2 messages were moved here from #new members > Compute roots of polynomials by Riccardo Brasca.

[Damiano Testa]

Scott, I tried pointing the lakefile to the fork of standard on my GitHub, but I do not think that it worked. Also, lake build decided that it was done when it reached

[1828/4223] Building Mathlib.CategoryTheory.Localization.Resolution
[1828/4223] Building Mathlib.CategoryTheory.Localization.Composition
[1830/4223] Building Mathlib.CategoryTheory.Localization.FiniteProducts

and returned me to the command line.

[François G. Dorais]

Run lake build again to see the error file.

[Damiano Testa]

Ok, it seems that the error were two lemmas that had already been defined. I'll keep building, seeing if I find some issues actually caused by not having Rat.ext.