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 intomul_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
andmul_lt_one_of_lt_one_of_le_one'
are applications ofmul_lt_of_lt_of_le_one
@[to_additive] lemma mul_lt_one'
is an application ofmul_lt_of_lt_of_lt_one
-- Lemma@[to_additive] lemma mul_eq_one_iff_eq_one_of_one_le
changed name tomul_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`.)
-->