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 <881fc59b2ec84f38153d9ae9c0b214e31ce61de4@gmail.com>

leanprover-community/mathlib,leanprover-community/mathlib