Commit 2021-10-08 07:33 639a7ef4

View on Github →

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.)

Estimated changes

Modified src/algebra/order/ring.lean

modified theorem mul_sub'

added theorem mul_sub_ge

modified theorem sub_mul'

added theorem sub_mul_ge

Modified src/data/real/ennreal.lean

deleted theorem ennreal.sub_mul_ge

Modified src/topology/instances/ennreal.lean