Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-04-11 16:16 e1feab4e

View on Github →

refactor(*): rename ordered groups/monoids to ordered add_ groups/monoids (#2347) In the perfectoid project we need ordered commutative monoids, and they are multiplicative. So the additive versions should be renamed to make some place.

Estimated changes

modified theorem with_top.sum_lt_top
modified theorem with_top.sum_lt_top_iff
modified theorem add_monoid.smul_nonneg
deleted theorem nonneg_comm_group.pos_def
modified theorem with_bot.add_bot
modified theorem with_bot.bot_add
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 with_top.zero_lt_coe
modified theorem with_top.zero_lt_top
modified theorem finsupp.add_eq_zero_iff
modified theorem finsupp.le_iff