Commit 2021-08-11 11:38 8d0ed030
View on Github →feat(data/rat/basic): Add nat num and denom inv lemmas (#8581)
Add inv_coe_nat_num and inv_coe_nat_denom lemmas.
These lemmas show that the denominator and numerator of 1/ n given 0 < n, are equal to n and 1 respectively.