RationalNumbers
Generated from the engine's own definition: compute-engine's symbol, which we neither extend nor document by hand. No examples yet — the crosswalk is the reason it has a page.
The set of all finite rational numbers.
mathlib4
RatRationalNumbers: set<rational>a constant, as compute-engine declares it