mathlib

639a7ef4 - feat(algebra/order/ring): variants of mul_sub' (#9604)

feat(algebra/order/ring): variants of mul_sub' (#9604) Add some variants of `mul_sub'` and `sub_mul'` and use them in `ennreal`. (Also sneaking in a tiny stylistic change in `topology/ennreal`.)