Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2018-08-21 21:22 82512ee8

View on Github →

refactor(analysis/ennreal): use canonically_ordered_comm_semiring (with_top α)

Estimated changes

added theorem with_top.add_top
added theorem with_top.coe_add
added theorem with_top.coe_ne_top
added theorem with_top.top_add
added theorem with_top.top_ne_coe
added theorem option.bind_comm
added theorem with_top.coe_eq_zero
added theorem with_top.coe_mul_coe
added theorem with_top.coe_zero
added theorem with_top.mul_coe
added theorem with_top.mul_def
added theorem with_top.mul_top
added theorem with_top.none_eq_top
added theorem with_top.some_eq_coe
added theorem with_top.top_mul
added theorem with_top.top_ne_zero
added theorem with_top.zero_eq_coe
added theorem with_top.zero_ne_top
modified theorem ennreal.infty_ne_of_real
modified theorem ennreal.infty_ne_zero
modified theorem ennreal.of_real_ne_infty
modified theorem ennreal.zero_ne_infty
added def ennreal
deleted inductive ennreal