Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-12-15 21:28 7cda8bb1

View on Github →

feat(data/real/ennreal): more lemmas, *_cast tags, use lift tactic (#1754)

  • feat(data/real/ennreal): more lemmas, *_cast tags, use lift tactic
  • Undo name change
  • Fix compile
  • nnreal: add move_cast
  • ennreal: more lemmas
  • Fix compile

Estimated changes

modified theorem ennreal.coe_div
added theorem ennreal.coe_inv_two
modified theorem ennreal.coe_le_one_iff
added theorem ennreal.coe_lt_coe_nat
modified theorem ennreal.coe_lt_one_iff
modified theorem ennreal.coe_nat
added theorem ennreal.coe_nat_lt_coe
added theorem ennreal.coe_nat_ne_top
added theorem ennreal.coe_sub_infty
added theorem ennreal.coe_two
modified theorem ennreal.div_self
added theorem ennreal.div_top
added theorem ennreal.inv_lt_one
added theorem ennreal.inv_mul_cancel
added theorem ennreal.inv_one
added theorem ennreal.max_mul
added theorem ennreal.mul_div_cancel
modified theorem ennreal.mul_inv_cancel
deleted theorem ennreal.mul_le_if_le_inv
added theorem ennreal.mul_le_mul
added theorem ennreal.mul_left_mono
added theorem ennreal.mul_max
added theorem ennreal.mul_ne_top
added theorem ennreal.mul_right_mono
added theorem ennreal.mul_sub
modified theorem ennreal.one_le_coe_iff
modified theorem ennreal.one_lt_coe_iff
added theorem ennreal.one_lt_two
added theorem ennreal.pow_eq_top
added theorem ennreal.pow_lt_top
added theorem ennreal.pow_ne_top
added theorem ennreal.sub_half
added theorem ennreal.sub_mul
modified theorem ennreal.to_nnreal_coe
added theorem ennreal.top_div
added theorem ennreal.top_pow
added theorem ennreal.two_ne_top
added theorem ennreal.two_ne_zero
added theorem ennreal.two_pos
added theorem ennreal.zero_div
modified theorem ennreal.zero_lt_coe_iff
added theorem nnreal.inv_one
added theorem nnreal.two_inv_lt_one