ennreal): weaker assumptions in `sub_mul`, add `coe_inv_le` (#2074)

Commit

5 years ago

chore(data/real/ennreal): weaker assumptions in `sub_mul`, add `coe_inv_le` (#2074) Co-authored-by: mergify[bot] <37929162+mergify[bot]@users.noreply.github.com>

References

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

Author

urkud

Parents

bfbd0937

mathlib3 62756bd3 - chore(data/real/ennreal): weaker assumptions in `sub_mul`, add `coe_inv_le` (#2074)

mathlib3
62756bd3 - chore(data/real/ennreal): weaker assumptions in `sub_mul`, add `coe_inv_le` (#2074)