Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-11-22 22:06 20444517

View on Github →

chore(data/real/ennreal): add a few lemmas (#5071) Also swap LHS with RHS in to_real_mul_to_real and rename it to to_real_mul.

Estimated changes

modified theorem ennreal.add_lt_add_iff_left
modified theorem ennreal.div_eq_top
modified theorem ennreal.div_le_iff_le_mul
modified theorem ennreal.div_lt_top
modified theorem ennreal.div_pos_iff
modified theorem ennreal.div_zero_iff
modified theorem ennreal.exists_nat_mul_gt
modified theorem ennreal.half_lt_self
modified theorem ennreal.infi_mul
modified theorem ennreal.inv_le_iff_le_mul
modified theorem ennreal.inv_lt_top
modified theorem ennreal.inv_top
modified theorem ennreal.le_div_iff_mul_le
modified theorem ennreal.lt_add_right
modified theorem ennreal.mem_Iio_self_add
modified theorem ennreal.mul_eq_mul_left
modified theorem ennreal.mul_eq_top
modified theorem ennreal.mul_infi
modified theorem ennreal.mul_inv_cancel
modified theorem ennreal.mul_le_iff_le_inv
modified theorem ennreal.mul_le_mul_left
modified theorem ennreal.mul_lt_mul_left
modified theorem ennreal.mul_lt_top
modified theorem ennreal.mul_lt_top_iff
modified theorem ennreal.nat_ne_top
modified theorem ennreal.none_eq_top
modified theorem ennreal.not_top_le_coe
modified theorem ennreal.sub_right_inj
modified theorem ennreal.supr_coe_nat
modified theorem ennreal.to_nnreal_add
modified theorem ennreal.to_nnreal_sum
modified theorem ennreal.to_real_add
modified theorem ennreal.to_real_eq_to_real
modified theorem ennreal.to_real_eq_zero_iff
modified theorem ennreal.to_real_le_to_real
modified theorem ennreal.to_real_lt_to_real
modified theorem ennreal.to_real_max
added theorem ennreal.to_real_mul
modified theorem ennreal.to_real_mul_top
added theorem ennreal.to_real_pow
added theorem ennreal.to_real_prod
modified theorem ennreal.to_real_sum
modified theorem ennreal.to_real_top_mul
modified theorem ennreal.top_div_of_lt_top
modified theorem ennreal.top_div_of_ne_top
modified theorem ennreal.top_ne_nat