chore(Algebra/Order/BigOperators): follow the ₀ naming convention

[YaelDillies]

We have long agreed that MonoidWithZero lemmas corresponding to Monoid lemmas should be suffixed with ₀, while currently it is the Monoid lemmas that are primed.

Also deprecate two primed lemmas that only differed from the unprimed versions in a minor way.

Renames

Moves:

• finprod_le_finprod -> finprod_le_finprod'
• finprod_le_finprod₀ -> finprod_le_finprod
• Finset.prod_le_prod -> Finset.prod_le_prod'
• Finset.one_le_prod -> Finset.one_le_prod'
• Finset.prod_le_one -> Finset.prod_le_one'
• Finset.prod_le_prod_of_subset_of_one_le -> Finset.prod_le_prod_of_subset_of_one_le'
• Finset.prod_le_prod_of_subset_of_le_one -> Finset.prod_le_prod_of_subset_of_le_one'
• Finset.prod_mono_set_of_one_le -> Finset.prod_mono_set_of_one_le'
• Finset.prod_anti_set_of_le_one -> Finset.prod_anti_set_of_le_one'
• Finset.prod_le_univ_prod_of_one_le -> Finset.prod_le_univ_prod_of_one_le'
• Finset.prod_eq_one_iff_of_one_le -> Finset.prod_eq_one_iff_of_one_le'
• Finset.prod_eq_one_iff_of_le_one -> Finset.prod_eq_one_iff_of_le_one'
• Finset.single_le_prod -> Finset.single_le_prod'
• Finset.prod_fiberwise_le_prod_of_one_le_prod_fiber -> Finset.prod_fiberwise_le_prod_of_one_le_prod_fiber'
• Finset.prod_le_prod_fiberwise_of_prod_fiber_le_one -> Finset.prod_le_prod_fiberwise_of_prod_fiber_le_one'
• Finset.prod_le_prod_of_subset -> Finset.prod_le_prod_of_subset'
• Finset.prod_mono_set -> Finset.prod_mono_set'
• Finset.prod_le_prod_of_ne_one -> Finset.prod_le_prod_of_ne_one'
• Finset.prod_lt_prod -> Finset.prod_lt_prod'
• Finset.prod_lt_prod_of_nonempty -> Finset.prod_lt_prod_of_nonempty'
• Finset.prod_lt_prod_of_subset -> Finset.prod_lt_prod_of_subset'
• Finset.single_lt_prod -> Finset.single_lt_prod'
• Finset.exists_lt_of_prod_lt -> Finset.exists_lt_of_prod_lt'
• Finset.exists_le_of_prod_le -> Finset.exists_le_of_prod_le'
• Finset.exists_one_lt_of_prod_one_of_exists_ne_one -> Finset.exists_one_lt_of_prod_one_of_exists_ne_one'
• Fintype.prod_mono -> Fintype.prod_mono'
• Fintype.prod_strictMono -> Fintype.prod_strictMono'
• List.Forall₂.prod_le_prod -> List.Forall₂.prod_le_prod'
• List.Sublist.prod_le_prod -> List.Sublist.prod_le_prod'
• List.SublistForall₂.prod_le_prod -> List.SublistForall₂.prod_le_prod'
• List.prod_le_prod -> List.prod_le_prod'
• List.prod_lt_prod -> List.prod_lt_prod'
• List.exists_lt_of_prod_lt -> List.exists_lt_of_prod_lt'
• List.exists_le_of_prod_le -> List.exists_le_of_prod_le'
• Multiset.prod_lt_prod -> Multiset.prod_lt_prod'
• Multiset.prod_lt_prod_of_nonempty -> Multiset.prod_lt_prod_of_nonempty'
• Finset.prod_le_prod₀ -> Finset.prod_le_prod
• Finset.prod_le_one₀ -> Finset.prod_le_one
• Finset.one_le_prod₀ -> Finset.one_le_prod
• Finset.prod_le_prod_of_subset_of_one_le₀ -> Finset.prod_le_prod_of_subset_of_one_le
• Finset.prod_le_prod_of_subset_of_le_one₀ -> Finset.prod_le_prod_of_subset_of_le_one
• Finset.prod_mono_set_of_one_le₀ -> Finset.prod_mono_set_of_one_le
• Finset.prod_anti_set_of_le_one₀ -> Finset.prod_anti_set_of_le_one
• Finset.prod_lt_prod₀ -> Finset.prod_lt_prod
• Finset.prod_lt_prod_of_nonempty₀ -> Finset.prod_lt_prod_of_nonempty

Deprecations

• Finset.sum_nonneg', Finset.one_le_prod''

Zulip

---

[github-actions]

PR summary 1ea4ecf9ad

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff

+ Forall₂.prod_le_prod
+ Sublist.prod_le_prod
+ SublistForall₂.prod_le_prod
+ exists_one_lt_of_prod_one_of_exists_ne_one
+ finprod_le_finprod₀
+ one_le_prod₀
+ prod_anti_set_of_le_one₀
+ prod_eq_one_iff_of_le_one
+ prod_eq_one_iff_of_one_le
+ prod_fiberwise_le_prod_of_one_le_prod_fiber
+ prod_le_one₀
+ prod_le_prod_fiberwise_of_prod_fiber_le_one
+ prod_le_prod_of_ne_one
+ prod_le_prod_of_subset
+ prod_le_prod_of_subset_of_le_one₀
+ prod_le_prod_of_subset_of_one_le₀
+ prod_le_prod₀
+ prod_le_univ_prod_of_one_le
+ prod_lt_prod_of_nonempty₀
+ prod_lt_prod_of_subset
+ prod_lt_prod₀
+ prod_mono
+ prod_mono_set
+ prod_mono_set_of_one_le₀
+ prod_strictMono
+ single_le_prod
+ single_lt_prod
++ exists_le_of_prod_le
++ exists_lt_of_prod_lt
+++--- prod_lt_prod'
++-- exists_le_of_prod_le'
++-- exists_lt_of_prod_lt'
++-- prod_le_prod'
++-- prod_lt_prod_of_nonempty'
+--+ one_le_prod
- prod_le_one'
-++ prod_le_prod
-++ prod_lt_prod_of_nonempty
-+++ prod_lt_prod
-+-+ prod_le_one

You can run this locally as follows

## from your `mathlib4` directory:
git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci

## summary with just the declaration names:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh <optional_commit>

## more verbose report:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh long <optional_commit>

The doc-module for scripts/pr_summary/declarations_diff.sh in the mathlib-ci repository contains some details about this script.

---

No changes to strong technical debt.

No changes to weak technical debt.

[mathlib-merge-conflicts]

This pull request has conflicts, please merge master and resolve them.

[b-mehta]

As I mentioned to you previously, I don't think this PR is a helpful one right now. The ₀ naming convention is not documented, and is followed the minority of the time in mathlib, in particular not even followed consistently in the MonoidWithZero and GroupWithZero.
On the other hand, the local ' convention for big operator lemmas around groups and rings is followed consistently, and even has the local benefit that the Finset.prod lemmas for CommMonoid are primed, meaning that the Finset.sum lemmas for AddCommGroup are not, and that the Finset.prod lemmas for CommMonoidWithZero are not. And these latter two categories are the more commonly used ones, so they have shorter names!

As a result, this PR:
a) Claims "long agreed" with no reference to prior discussion or agreement
b) It starts a new local convention, making things more globally inconsistent, and locally less convenient
c) Doesn't list what renames are happening, meaning downstream users will find it hard to adapt, in particular because you are replacing old names - note that this explicitly documented as discouraged for contributors
d) Doesn't list what's being deprecated in the PR description

I understand that some of these may take a couple of minutes out of your day, but all of these points make things significantly easier for reviewers, and for downstream users to adjust to your (breaking) changes.

[vihdzp]

I'm surprised that the subscript zero isn't documented. Can we document it somewhere and ensure it's followed? Or failing that, can we figure out some other consistent way to name results that are "morally the same as other results about groups except for the fact 0 is involved"?

[YaelDillies]

Here is a PR to the naming convention documenting the ₀ suffix: leanprover-community/leanprover-community.github.io#870

[Vierkantor]

Thanks! In addition to looking at the diff, I searched for prod' in Mathlib and confirmed the remaining primed prod lemmas have this for a non-WithZero reason.

bors r+

[Vierkantor]

bors r-

[mathlib-bors]

Bors build canceled.

Address comments or fix if necessary, and then someone with permission can run bors r+.

[Vierkantor]

This is awaiting leanprover-community/leanprover-community.github.io#870.

[b-mehta]

It looks like the renames section is backwards from the diff. It also looks like some deprecations are missing, from a quick skim-through I noticed Finset.abs_sum_of_nonneg', for instance