Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-03-17 01:31 496939ce

View on Github →

feat(data/real/*nnreal): add division lemmas (#2167)

  • feat(data/real/*nnreal): add division lemmas
  • fix build
  • elim_cast
  • another elim_cast

Estimated changes

deleted theorem ennreal.coe_sub_infty
added theorem ennreal.div_eq_top
modified theorem ennreal.div_le_iff_le_mul
added theorem ennreal.div_one
modified theorem ennreal.le_div_iff_mul_le
added theorem ennreal.mul_div_assoc
modified theorem ennreal.none_eq_top
modified theorem ennreal.some_eq_coe
added theorem nnreal.add_div'
added theorem nnreal.coe_ne_zero
added theorem nnreal.div_add'
added theorem nnreal.div_add_div
added theorem nnreal.div_eq_div_iff
added theorem nnreal.div_eq_iff
added theorem nnreal.div_lt_iff
added theorem nnreal.div_pow
added theorem nnreal.eq_div_iff
added theorem nnreal.inv_eq_one_div
added theorem nnreal.mul_div_assoc'
added theorem nnreal.mul_ne_zero'
added theorem nnreal.one_div_div
added theorem nnreal.one_div_eq_inv
added theorem nnreal.pow_eq_zero
added theorem nnreal.pow_ne_zero