Commit 2024-02-22 09:41 d67f7a69
View on Github →feat: Add mul_inv
and inv_mul
versions of div_le_one_of_le
(#10597)
These are exactly div_le_one_of_le
with a / b
replaced by a * b⁻¹
and b⁻¹ * a
.
They come up frequently because some tactics produce inverses as normal forms over division. The iff versions with 0 < b
already exist as mul_inv_le_one_iff
and inv_mul_le_one_iff
; the point of these is to have a weaker nonnegativity assumption on b
.