mathlib
795d5ab6 - chore(algebra/ordered_monoid): rename lemmas (#5657)

Commit
4 years ago
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.
Author
Parents
Loading