Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-09-25 14:53 565efec2

View on Github →

chore(data/real/ennreal): 3 lemmas stating ∞ / b = ∞ (#4248)

Estimated changes

Modified src/data/real/ennreal.lean

added theorem ennreal.top_div_coe

added theorem ennreal.top_div_of_lt_top

added theorem ennreal.top_div_of_ne_top