Commit 2026-09-04 14:00 a78f66ab

View on Github →

chore(Algebra/Order/BigOperators): follow the ₀ naming convention (#39692) The naming convention stipulates that MonoidWithZero lemmas corresponding to Monoid lemmas should be suffixed with ₀, but currently in the big operators API it is the Monoid lemmas that are primed. This PR unprimes the Monoid lemmas and appends ₀ to the MonoidWithZero lemmas. 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.one_le_prod'' → Finset.one_le_prod
Finset.sum_nonneg' → Finset.sum_nonneg
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.abs_sum_of_nonneg' → Finset.abs_sum_of_nonneg
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
Finset.prod_le_prod_of_injOn' → Finset.prod_le_prod_of_injOn
Finset.prod_le_prod_of_injOn → Finset.prod_le_prod_of_injOn₀
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₀