Commit 2026-03-05 14:29 0ff022a7

feat(Algebra/Order/BigOperators): order properties of subsets in groups with zero (#35008) We have these lemmas for CommMonoid, but not yet for CommMonoidWithZero. We rename the CommMonoid versions, for consistency with all the surrounding lemmas: the local convention here is for the CommMonoid version to have primes, and the AddCommMonoid and CommMonoidWithZero versions not to (since the latter applies in the more common case of rings). The explicit changes are:

• prod_le_prod_of_subset_of_le_one -> prod_le_prod_of_subset_of_le_one'
• prod_anti_set_of_le_one -> prod_anti_set_of_le_one' In both cases, the old name is reused for the version in CommMonoidWithZero.
• depends on: #35005