Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-04-07 08:48 d936c288

View on Github →

feat(data/real/nnreal): coe_max and coe_min (#2346)

Estimated changes

added theorem nnreal.coe_max
added theorem nnreal.coe_min