Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-01-08 09:47 795d5ab6

View on Github →

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.

Estimated changes

deleted theorem le_one_iff_eq
added theorem le_one_iff_eq_one
modified theorem one_lt_iff_ne_one
added theorem self_le_mul_left
added theorem self_le_mul_right
deleted theorem cardinal.add_le_add
deleted theorem cardinal.add_le_add_left
deleted theorem cardinal.add_le_add_right
deleted theorem cardinal.le_add_left
deleted theorem cardinal.le_add_right
deleted theorem cardinal.le_zero
deleted theorem cardinal.mul_le_mul
deleted theorem cardinal.mul_le_mul_left
deleted theorem cardinal.mul_le_mul_right
deleted theorem cardinal.pos_iff_ne_zero
deleted theorem cardinal.zero_le