Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-06-23 09:25 47ed97f3

View on Github →

feat(algebra/ordered_monoid_lemmas + fixes): consistent use of covariant and contravariant in ordered_monoid_lemmas (#7876) This PR breaks off a part of PR #7645. Here, I start using more consistently covariant_class and contravariant_class in the file algebra/ordered_monoid_lemmas. This PR is simply intended as a stepping stone to merging the bigger one (#7645) and receiving "personalized comments on it!

Summary of changes:

New lemmas

  • @[to_additive add_nonneg] lemma one_le_mul_right
  • @[to_additive] lemma le_mul_of_le_of_le_one
  • @[to_additive] lemma mul_lt_mul_of_lt_of_lt
  • @[to_additive] lemma left.mul_lt_one_of_lt_of_lt_one
  • @[to_additive] lemma right.mul_lt_one_of_lt_of_lt_one
  • @[to_additive] lemma left.mul_lt_one_of_lt_of_lt_one
  • @[to_additive] lemma right.mul_lt_one_of_lt_of_lt_one
  • @[to_additive right.add_nonneg] lemma right.one_le_mul
  • @[to_additive right.pos_add] lemma right.one_lt_mul -- Lemmas that have merged with their unprimed versions due to diminished typeclass assumptions
  • @[to_additive] lemma lt_mul_of_one_le_of_lt'
  • @[to_additive] lemma lt_mul_of_one_lt_of_lt'
  • @[to_additive] lemma mul_le_of_le_of_le_one'
  • @[to_additive] lemma mul_le_of_le_one_of_le'
  • @[to_additive] lemma mul_lt_of_lt_of_le_one'
  • @[to_additive] lemma mul_lt_of_lt_of_lt_one'
  • @[to_additive] lemma mul_lt_of_lt_one_of_lt'
  • the three lemmas
    • @[to_additive] lemma mul_lt_of_le_one_of_lt',
    • mul_lt_one_of_le_one_of_lt_one,
    • mul_lt_one_of_le_one_of_lt_one' all merged into mul_lt_of_le_one_of_lt -- Lemma @[to_additive] lemma mul_lt_one broke into
  • @[to_additive] lemma left.mul_lt_one
  • @[to_additive] lemma right.mul_lt_one depending on typeclass assumptions -- Lemmas that became a direct application of another lemma
  • @[to_additive] lemma mul_lt_one_of_lt_one_of_le_one and mul_lt_one_of_lt_one_of_le_one' are applications of mul_lt_of_lt_of_le_one
  • @[to_additive] lemma mul_lt_one' is an application of mul_lt_of_lt_of_lt_one -- Lemma @[to_additive] lemma mul_eq_one_iff_eq_one_of_one_le changed name to mul_eq_one_iff_eq_one_of_one_le. The multiplicative version is never used. The additive version, add_eq_zero_iff_eq_zero_of_nonneg is used: I changed the occurrences in favour of the shorter name. -- Lemma @[to_additive add_nonpos] lemma mul_le_one' continues as
alias mul_le_of_le_of_le_one ← mul_le_one'
attribute [to_additive add_nonpos] mul_le_one'
<!-- Name changes: * lemma `mul_le_of_le_one_of_le'` became `mul_le_of_le_one_of_le`; * lemma `lt_mul_of_one_le_of_lt'` became `lt_mul_of_one_le_of_lt`; * lemma `add_eq_zero_iff_eq_zero_of_nonneg` became `add_eq_zero_iff'`. (Really, the lemmas above are the ones that were used outside of the PR: the two `mul` ones have a corresponding `to_additive` version and the `add` one is the `to_additive` version of `mul_eq_one_iff_eq_one_of_one_le`.) -->

Estimated changes

modified theorem le_mul_iff_one_le_left'
modified theorem le_mul_iff_one_le_right'
added theorem le_mul_of_le_of_le_one
modified theorem le_mul_of_one_le_of_le
modified theorem le_mul_of_one_le_right'
modified theorem le_of_mul_le_mul_left'
modified theorem le_of_mul_le_mul_right'
added theorem left.mul_lt_one
modified theorem lt_mul_iff_one_lt_left'
modified theorem lt_mul_iff_one_lt_right'
modified theorem lt_mul_of_le_of_one_lt
modified theorem lt_mul_of_lt_of_one_le
modified theorem lt_mul_of_lt_of_one_lt
deleted theorem lt_mul_of_one_le_of_lt'
modified theorem lt_mul_of_one_lt_left'
modified theorem lt_mul_of_one_lt_of_le
deleted theorem lt_mul_of_one_lt_of_lt'
modified theorem lt_mul_of_one_lt_right'
modified theorem lt_of_mul_lt_mul_left'
modified theorem monotone.const_mul'
modified theorem monotone.mul'
modified theorem monotone.mul_const'
modified theorem monotone.mul_strict_mono'
modified theorem mul_le_iff_le_one_left'
modified theorem mul_le_iff_le_one_right'
modified theorem mul_le_mul_iff_left
modified theorem mul_le_mul_iff_right
modified theorem mul_le_mul_left'
modified theorem mul_le_mul_right'
modified theorem mul_le_mul_three
deleted theorem mul_le_of_le_of_le_one'
modified theorem mul_le_of_le_of_le_one
deleted theorem mul_le_of_le_one_of_le'
modified theorem mul_le_of_le_one_of_le
modified theorem mul_le_of_le_one_right'
deleted theorem mul_le_one'
modified theorem mul_lt_iff_lt_one_left'
modified theorem mul_lt_iff_lt_one_right'
modified theorem mul_lt_mul_iff_left
modified theorem mul_lt_mul_iff_right
modified theorem mul_lt_mul_left'
modified theorem mul_lt_mul_of_le_of_lt
modified theorem mul_lt_mul_of_lt_of_le
added theorem mul_lt_mul_of_lt_of_lt
modified theorem mul_lt_mul_right'
modified theorem mul_lt_of_le_of_lt_one
deleted theorem mul_lt_of_le_one_of_lt'
modified theorem mul_lt_of_le_one_of_lt
deleted theorem mul_lt_of_lt_of_le_one'
modified theorem mul_lt_of_lt_of_le_one
deleted theorem mul_lt_of_lt_of_lt_one'
modified theorem mul_lt_of_lt_of_lt_one
modified theorem mul_lt_of_lt_one_of_le
deleted theorem mul_lt_of_lt_one_of_lt'
modified theorem mul_lt_of_lt_one_of_lt
deleted theorem mul_lt_one'
deleted theorem mul_lt_one
modified theorem one_le_mul
added theorem one_le_mul_right
added theorem right.mul_lt_one
added theorem right.one_le_mul
added theorem right.one_lt_mul