Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-11-24 17:44 ca53b5d5

View on Github →

feat(data/real/ennreal): 3 simple lemmas (#1734)

Estimated changes

Modified src/data/real/ennreal.lean

added theorem ennreal.coe_to_real

added theorem ennreal.to_nnreal_pos_iff

added theorem ennreal.to_real_pos_iff