Commit 2022-09-02 10:49 86152105
View on Github →feat(data/rat/defs): inv_coe_{int,nat}_{num,denom} (#15863)
Rename existing lemmas to
inv_coe_{int,nat}_{num,denom}_of_pos
since they took positivity assumptions
Also provide rat.inv_neg
.
feat(data/rat/defs): inv_coe_{int,nat}_{num,denom} (#15863)
Rename existing lemmas to
inv_coe_{int,nat}_{num,denom}_of_pos
since they took positivity assumptions
Also provide rat.inv_neg
.