Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-10-31 15:07 9a03bdf1

View on Github →

chore(algebra/ordered_group): use implicit args, add add_eq_coe (#4853)

  • Use implicit arguments in various iff lemmas about with_top.
  • Add add_eq_coe.
  • Rewrite with_top.ordered_add_comm_monoid moving begin .. end blocks inside the structure. This way we don't depend on the fact that refine doesn't introduce any ids and it's easier to see right away which block proves which statement.

Estimated changes

added theorem with_top.add_eq_coe
modified theorem with_top.add_eq_top
modified theorem with_top.add_lt_top
modified theorem with_top.add_top
modified theorem with_top.top_add
modified theorem ennreal.add_eq_top
modified theorem ennreal.add_lt_top
added theorem ennreal.coe_finset_sup
modified theorem ennreal.coe_le_iff
modified theorem ennreal.le_coe_iff
modified theorem ennreal.lt_iff_exists_coe
modified theorem with_top.coe_le_iff
added theorem with_top.coe_lt_iff
modified theorem with_top.le_coe_iff
modified theorem with_top.lt_iff_exists_coe