Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-03-02 16:19 62756bd3

View on Github →

chore(data/real/ennreal): weaker assumptions in sub_mul, add coe_inv_le (#2074)

Estimated changes

added theorem ennreal.coe_inv_le
modified theorem ennreal.mul_sub
modified theorem ennreal.sub_mul
added theorem ennreal.sub_mul_ge