Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-05-10 05:20 b17070db

View on Github →

fix(data/real/ennreal): style and golfing (#14055)

Estimated changes

modified theorem ennreal.coe_inv_two
modified theorem ennreal.inv_one
modified theorem ennreal.mul_left_mono
modified theorem ennreal.mul_right_mono