Mathlib v3 is deprecated. Go to Mathlib v4

Theorem inv_mul_lt_of_lt_mul₀

Modification history

2021-10-06 10:12
src/algebra/order/with_zero.lean
feat(topology/algebra): topology on a linear_ordered_comm_group_with_zero (#9537) …
Added inv_mul_lt_of_lt_mul₀View on Github →