Skip to content

feat(Algebra/Order): maximally varying version of prod_le_prod_of_subset_of_one_le#39646

Open
YaelDillies wants to merge 2 commits into
leanprover-community:masterfrom
YaelDillies:prod_le_prod_of_subset_of_one_le
Open

feat(Algebra/Order): maximally varying version of prod_le_prod_of_subset_of_one_le#39646
YaelDillies wants to merge 2 commits into
leanprover-community:masterfrom
YaelDillies:prod_le_prod_of_subset_of_one_le

Conversation

@YaelDillies

@YaelDillies YaelDillies commented May 21, 2026 •
edited
Loading

Copy link
Copy Markdown
Contributor

@YaelDillies YaelDillies added the t-algebra Algebra (groups, rings, fields, etc) label May 21, 2026
@github-actions

github-actions Bot commented May 21, 2026 •
edited
Loading

Copy link
Copy Markdown

PR summary 00c982ae50

Import changes for modified files

No significant changes to the import graph

Import changes for all files
Files Import difference

Declarations diff

+ prod_mono_of_subset_of_le_one
+ prod_mono_of_subset_of_le_one₀
+ prod_mono_of_subset_of_one_le
+ prod_mono_of_subset_of_one_le₀

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.

b-mehta
b-mehta requested changes May 21, 2026
View reviewed changes
Comment thread Mathlib/Algebra/Order/BigOperators/Group/Finset.lean
@YaelDillies YaelDillies force-pushed the prod_le_prod_of_subset_of_one_le branch from e86ff5d to 741edb4 Compare May 21, 2026 09:25
@YaelDillies YaelDillies changed the title chore(Algebra): generalise prod_le_prod_of_subset_of_one_le feat(Algebra/Order): maximally varying version of prod_le_prod_of_subset_of_one_le May 21, 2026
b-mehta
b-mehta requested changes May 21, 2026
View reviewed changes
Comment thread Mathlib/Algebra/Order/BigOperators/Group/Finset.lean
theorem prod_le_prod_of_subset_of_one_le' [MulLeftMono N] (h : s ⊆ t)
(hf : ∀ i ∈ t, i ∉ s → 1 ≤ f i) : ∏ i ∈ s, f i ≤ ∏ i ∈ t, f i := by
@[to_additive (attr := gcongr)]
lemma prod_mono_of_subset_of_one_le [MulLeftMono N] (h : s ⊆ t) (hfg : ∀ i ∈ s, f i ≤ g i)

@b-mehta b-mehta May 21, 2026

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This one should have a prime in the name, since that's the established naming convention for these lemmas.
I'm conscious that you would like to enforce your personal new ₀ convention, but this is not widely applied, and never applied for finset lemmas, so let's not start new half-refactors.

@b-mehta b-mehta May 21, 2026

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

In addition, the renames are clearly scope-creep!

@YaelDillies YaelDillies May 22, 2026

Copy link
Copy Markdown
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

See #39692

themathqueen
themathqueen reviewed Jun 18, 2026
View reviewed changes
Comment thread Mathlib/Algebra/Module/ZLattice/Summable.lean

@themathqueen themathqueen Jun 18, 2026 •
edited
Loading

Copy link
Copy Markdown
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I'm not entirely sure where this PR stands because of @b-mehta's comments in both here and #39692, so I'm not sure what to do.

But the golf here looks fine and doesn't use anything else in the PR, so

splice-bot maintainer merge

@mathlib-splicebot mathlib-splicebot Bot Jun 18, 2026

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Unknown splice-bot command

No label command matched keyword 'maintainer-merge'.

Failed step(s): Resolve configured trigger command.

Advice:

  • Either remove the keyword to run the default split-PR flow, or add a matching entry to label_commands.

Run logs: https://github.com/leanprover-community/mathlib4/actions/runs/27756166287/attempts/1

Step outcomes
  • Consume bridge artifact: success
  • Fetch and parse trigger comment: success
  • Resolve configured trigger command: failure
  • Authorize commenter: success
  • Check out BASE: skipped
  • Check out HEAD: skipped
  • Stage file changes: skipped
  • Validate create-pull-request inputs: skipped
  • Create Pull Request: skipped
  • Apply label to split PR: skipped
  • Post comment on split PR: skipped
Token diagnostics
  • token source: inputs.token
  • branch token source: inputs.branch_token
  • authz token source: inputs.authz_token
  • commenter: themathqueen
  • pr author: YaelDillies
  • base repo: leanprover-community/mathlib4
  • allow_pr_author: true
  • min_repo_permission: disabled
  • observed_repo_permission: not-checked
  • allowed_users: (none)
  • allowed_teams: leanprover-community/mathlib-reviewers, leanprover-community/mathlib-maintainers
  • matched_rules: team:leanprover-community/mathlib-reviewers
  • authz token source: inputs.authz_token
  • trigger keyword: maintainer-merge
  • label authz token source: inputs.authz_token

@themathqueen themathqueen Jun 18, 2026

Copy link
Copy Markdown
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Don't think editing worked, might have to do this again:

splice-bot maintainer merge

@mathlib-splicebot mathlib-splicebot Bot Jun 18, 2026

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Split PR created and commented

Split off the changes to Mathlib/Algebra/Module/ZLattice/Summable.lean in #40752 and posted a comment via splice-bot command maintainer.

@mathlib-splicebot mathlib-splicebot Bot mentioned this pull request Jun 18, 2026
Closed
mathlib-bors Bot pushed a commit that referenced this pull request Jun 18, 2026
@mathlib-splicebot @YaelDillies
chore(Algebra/Module/ZLattice/Summable): automated extraction from #3…
4176265 
…9646 (#40752)

Author: Yaël Dillies <yael.dillies@gmail.com>

Co-authored-by: YaelDillies <14090593+YaelDillies@users.noreply.github.com>
@mathlib-dependent-issues mathlib-dependent-issues Bot added the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Jun 18, 2026
@mathlib-dependent-issues

mathlib-dependent-issues Bot commented Jun 18, 2026

Copy link
Copy Markdown

This PR/issue depends on:

ReemMelamed pushed a commit to ReemMelamed/mathlib4 that referenced this pull request Jun 20, 2026
@mathlib-splicebot @YaelDillies @ReemMelamed
chore(Algebra/Module/ZLattice/Summable): automated extraction from le…
2b84358 
…anprover-community#39646 (leanprover-community#40752)

Author: Yaël Dillies <yael.dillies@gmail.com>

Co-authored-by: YaelDillies <14090593+YaelDillies@users.noreply.github.com>
bryangingechen pushed a commit to jcommelin/mathlib4 that referenced this pull request Jun 22, 2026
@mathlib-splicebot @YaelDillies @bryangingechen
chore(Algebra/Module/ZLattice/Summable): automated extraction from le…
e87050a 
…anprover-community#39646 (leanprover-community#40752)

Author: Yaël Dillies <yael.dillies@gmail.com>

Co-authored-by: YaelDillies <14090593+YaelDillies@users.noreply.github.com>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@themathqueen themathqueen themathqueen left review comments
@b-mehta b-mehta b-mehta requested changes
+1 more reviewer
@mathlib-splicebot mathlib-splicebot[bot] mathlib-splicebot[bot] left review comments
Reviewers whose approvals may not affect merge requirements

Assignees

@themathqueen themathqueen

Labels

blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) t-algebra Algebra (groups, rings, fields, etc)

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

3 participants

@YaelDillies @themathqueen @b-mehta