Commit 2022-07-08 18:50 11cdccb8

View on Github →

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.

Estimated changes

Modified src/data/rat/defs.lean

added theorem rat.coe_pnat_denom

added theorem rat.mk_pnat_pnat_denom_eq

added def rat.pnat_denom

added theorem rat.pnat_denom_eq_iff_denom_eq