mathlib

11cdccb8 - feat(data/rat/defs): add denominator as pnat (#15101)

feat(data/rat/defs): add denominator as pnat (#15101) Option to bundle `x.denom` and `x.pos` into a pnat, which can be useful in defining functions using the denominator. Co-authored-by: Jon Eugster <eugster.jon@gmail.com>