mathlib
86152105 - feat(data/rat/defs): inv_coe_{int,nat}_{num,denom} (#15863)

Commit
3 years ago
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`. Co-authored-by: Yakov Pechersky <pechersky@users.noreply.github.com>
Author
Parents
Loading