Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-05-15 21:20 56442cf2

View on Github →

feat(data/nnreal): div and pow lemmas (#7471) from the liquid tensor experiment

Estimated changes

Modified src/data/real/nnreal.lean

added theorem nnreal.div_le_div_left

added theorem nnreal.div_le_div_left_of_le

added theorem nnreal.pow_mono_decr_exp