Commit 2021-01-08 09:47 795d5ab6

chore(algebra/ordered_monoid): rename lemmas (#5657) I wanted to add the alias pos_iff_ne_zero for zero_lt_iff_ne_zero, but then I saw a note already in the library to do this renaming. So I went ahead. le_zero_iff_eq -> nonpos_iff_eq_zero zero_lt_iff_ne_zero -> pos_iff_ne_zero le_one_iff_eq -> le_one_iff_eq_one measure.le_zero_iff_eq_zero' -> measure.nonpos_iff_eq_zero' There were various specific types that had their own custom pos_iff_ne_zero-lemma, which caused nameclashes. Therefore:

• remove nat.pos_iff_ne_zero
• Prove that cardinal forms a canonically_ordered_semiring, remove various special case lemmas
• There were lemmas cardinal.le_add_[left|right]. Generalized them to arbitrary canonically_ordered_monoids and renamed them to self_le_add_[left|right] (to avoid name clashes)
• I did not provide a canonically_ordered_monoid class for ordinal, since that requires quite some work (it's true, right?)
• protect various lemmas in cardinal and ordinal to avoid name clashes.