mathlib3

6de241f9 - feat(data/rat/nnrat): Nonnegative rationals (#16283)

feat(data/rat/nnrat): Nonnegative rationals (#16283) Define `nnrat`, the subtype of nonnegative rational numbers, and show it forms a `canonically_linear_ordered_semifield`.