naming of `a ≤ 1 → b ≤ 1 → a * b ≤ 1` lemmas

Stream: mathlib4

[Yuyang Zhao]

After further organizing #9250, the new PR is #17593. Some lemmas have incorrect or unsatisfactory names, but I think they should be kept in mathlib. The part of renaming and adding ZeroLEOneClass is split as #17623. I was asked to start a discussion about this PR.

There are counterparts of these lemmas for Monoid (docs#one_le_mul, docs#one_lt_mul_of_lt_of_le', ...) and some exactly the same lemmas that were introduced for OrderedSemiring and generalized later (docs#one_lt_mul, docs#mul_lt_one_of_nonneg_of_lt_one_left, docs#mul_le_one, ...). docs#mul_le_one has been deprecated and renamed to docs#mul_le_one₀. So I think these lemmas should be renamed rather than just deleted.

The deprecated lemmas in this PR are not used in any other files in mathlib, because the old names are hard to discover and the widespread lemmas are those introduced earlier for OrderedSemiring. In the future, we may deprecate those lemmas and use the newly introduced better names.

For lemmas that use ZeroLEOneClass, they have Monoid counterparts that are exactly the same except typeclass assumptions. Their new names are Monoid lemma names with suffix ₀.

Other lemmas can be distinguished by explicit arguments, so there is no need to use Left Right namespaces. This PR changes them to _left _right. This also specifies which positivity needs to be provided.

[Notification Bot]

A message was moved here from #mathlib4 > lt_mul_of_le_of_one_lt' by Yuyang Zhao.

[Jireh Loreaux]

Can you specify exactly what the new naming scheme is? It's not clear to me from your post above. Please give at least two examples with your explanation (along with the current names of those lemmas).

[Yuyang Zhao]

Looks like some of the names in #17623 PR descriptions have been deprecated in #22353. I will give examples using the names of lemmas from OrderedSemiring API, which are not deprecated.

For lemmas that use ZeroLEOneClass, they have Monoid counterparts that are exactly the same except typeclass assumptions. Their new names are Monoid lemma names with suffix ₀.

{Left, Right}.one_rel_mul_of_rel_of_rel₀, or {Left, Right}.one_rel_mul₀ if rel is the same. Left and Right versions differ only in typeclass assumptions, choose one of them to create an alias in _root_.

Example: The new name of docs#one_lt_mul_of_le_of_lt is one_lt_mul_of_le_of_lt₀. The old name makes the Monoid version have to be called docs#one_lt_mul_of_le_of_lt'. Hence this is also in line with the idea of using the suffix ₀ to reduce ' in names.

Other lemmas can be distinguished by explicit arguments, so there is no need to use Left Right namespaces. This PR changes them to _left _right. This also specifies which positivity needs to be provided.

mul_rel_one_of_rel_of_rel_{left, right}₀, or mul_rel_one_{left, right}₀ if rel is the same.

mul_lt_one_of_le_of_lt_of_pos_left and mul_lt_one_of_lt_of_le_of_pos_right are just because the original lemma proved weaker results with weaker typeclass assumptions. Now that the original lemmas have been deprecated, maybe they're not needed now.

Example: docs#mul_le_one₀ does not specify which positivity proof is needed, and the new name mul_le_one_right₀ does.

Example: The new name of docs#mul_lt_one_of_nonneg_of_lt_one_left is mul_lt_one_of_lt_of_le_left₀. This name is also more consistent with the Monoid version docs#mul_lt_one_of_lt_of_le.

[Notification Bot]

Scott Carnahan has marked this topic as resolved.

[Notification Bot]

Scott Carnahan has marked this topic as unresolved.

[Scott Carnahan]

Sorry, I hit the wrong spot on my phone.