Skip to content

refactor(Data.Finset.MulAntidiagonal): rename set-based mulAntidiagonal to setMulAntidiagonal#34551

Closed
IlPreteRosso wants to merge 16 commits intoleanprover-community:masterfrom
IlPreteRosso:HasMulAntidiagonal
Closed

refactor(Data.Finset.MulAntidiagonal): rename set-based mulAntidiagonal to setMulAntidiagonal#34551
IlPreteRosso wants to merge 16 commits intoleanprover-community:masterfrom
IlPreteRosso:HasMulAntidiagonal

Conversation

@IlPreteRosso
Copy link
Copy Markdown
Contributor

@IlPreteRosso IlPreteRosso commented Jan 28, 2026 •
edited
Loading

Prod.lean has a TODO (line 48) to add HasMulAntidiagonal, which would export mulAntidiagonal into Finset. This collides with the existing set-based Finset.mulAntidiagonal in MulAntidiagonal.lean (which takes explicit IsPWO arguments). The additive side has no collision because the typeclass exports antidiagonal vs the set-based addAntidiagonal.

The key issue is the @[simp] lemma mem_mulAntidiagonal: both the set-based and typeclass-based versions would register simp lemmas with the same name in Finset

This PR renames the set-based definitions to use a set prefix and renames all referencing theorems/lemmas. Deprecation aliases are added for the old names.

@github-actions github-actions bot added new-contributor This PR was made by a contributor with at most 5 merged PRs. Welcome to the community! t-algebra Algebra (groups, rings, fields, etc) labels Jan 28, 2026
@github-actions
Copy link
Copy Markdown

github-actions bot commented Jan 28, 2026 •
edited
Loading

PR summary 1b7f970756

Import changes for modified files

No significant changes to the import graph

Import changes for all files
Files Import difference

Declarations diff

+ setMulAntidiagonal
+ setSMulAntidiagonal
+ smulAntidiagonal
- SMulAntidiagonal
-+-+ mulAntidiagonal_mono_left

You can run this locally as follows 
## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

No changes to technical debt.

You can run this locally as

./scripts/technical-debt-metrics.sh pr_summary
  • The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
  • The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

kim-em
kim-em reviewed Jan 28, 2026
View reviewed changes
Comment thread Mathlib/Algebra/Order/Antidiag/Prod.lean Outdated
@kim-em kim-em added the awaiting-author A reviewer has asked the author a question or requested changes. label Jan 28, 2026
@github-actions github-actions bot added awaiting-author A reviewer has asked the author a question or requested changes. and removed awaiting-author A reviewer has asked the author a question or requested changes. labels Jan 28, 2026
@IlPreteRosso
Copy link
Copy Markdown
Contributor Author

IlPreteRosso commented Jan 28, 2026 •
edited
Loading

@kim-em There is a problem with name conflict

Two files define Finset.swap_mem_mulAntidiagonal:
MulAntidiagonal.lean - set-based API:



theorem swap_mem_mulAntidiagonal :
   x.swap ∈ mulAntidiagonal hs ht a ↔ x ∈ mulAntidiagonal ht hs a

Takes explicit IsPWO proofs for sets s and t, where

noncomputable def mulAntidiagonal (hs : s.IsPWO) (ht : t.IsPWO) (a : α) : Finset (α × α)

Prod.lean (this PR) - typeclass API:



theorem swap_mem_mulAntidiagonal :
   xy.swap ∈ mulAntidiagonal n ↔ xy ∈ mulAntidiagonal n


Uses HasMulAntidiagonal typeclass, where

class HasMulAntidiagonal (M : Type*) [Monoid M] where
  mulAntidiagonal : M → Finset (M × M)

Solution:

  • Name change (API change)?
  • Rename namespace?
  • Nested namespaces? (ew)

@IlPreteRosso IlPreteRosso requested a review from kim-em January 28, 2026 23:54
@kim-em kim-em removed their request for review January 30, 2026 00:37
@kim-em kim-em added the awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. label Jan 30, 2026
@github-actions github-actions bot removed the awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. label Jan 30, 2026
@IlPreteRosso IlPreteRosso changed the title feat(Algebra/Order/Antidiag): add HasMulAntidiagonal and apply @[to_additive] refactor(Data.Finset.*Antidiagonal): rename defs to set*Antidiagonal Jan 31, 2026
@Ruben-VandeVelde
Copy link
Copy Markdown
Contributor

Ruben-VandeVelde commented Jan 31, 2026

Please add deprecations

awaiting-author

@github-actions github-actions bot added the awaiting-author A reviewer has asked the author a question or requested changes. label Jan 31, 2026
@github-actions github-actions bot added the WIP Work in progress label Jan 31, 2026
@github-actions github-actions bot removed the WIP Work in progress label Jan 31, 2026
@IlPreteRosso IlPreteRosso changed the title refactor(Data.Finset.*Antidiagonal): rename defs to set*Antidiagonal refactor(Data.Finset.*Antidiagonal): rename defs to set*Antidiagonal and deprecates old names Jan 31, 2026
@IlPreteRosso IlPreteRosso changed the title refactor(Data.Finset.*Antidiagonal): rename defs to set*Antidiagonal and deprecates old names refactor(Data.Finset.*Antidiagonal): rename defs to set*Antidiagonal and deprecate old names in namespace Finset Jan 31, 2026
@github-actions github-actions bot removed the awaiting-author A reviewer has asked the author a question or requested changes. label Jan 31, 2026
@mathlib-merge-conflicts mathlib-merge-conflicts bot added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Feb 9, 2026
@mathlib-merge-conflicts
Copy link
Copy Markdown

mathlib-merge-conflicts bot commented Feb 9, 2026

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

@github-actions github-actions bot removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Feb 9, 2026
@IlPreteRosso IlPreteRosso requested a review from kim-em February 9, 2026 21:23
jcommelin
jcommelin reviewed Feb 18, 2026
View reviewed changes
Copy link
Copy Markdown
Member

@jcommelin jcommelin left a comment

Choose a reason for hiding this comment

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

  1. I can't make heads or tails of the first sentences of your PR description. Please rewrite it so that it makes sense for a reviewer who doesn't have all the context front-loaded. (To be honest, it reads like an AI-generated description after splitting a PR.)
  2. "This PR renames the set-based antidiagonal definitions to have a set prefix, distinguishing them from the typeclass-based API in Prod.lean." -- Can you make this explicit? Can you explain why we need this? How is the current setup failing you? Atm, it's not clear to me that we even need this.
  3. "Only definitions are renamed in this PR. Theorem/lemma renames will follow in a subsequent PR." -- Not a fan of that. The lemma names will be out of sync with their statements, because the name components don't match the names that occur in the statement. Since this PR is only doing one thing (i.e. renaming), let's just rename the entire API, if we come to the conclusion that renaming is needed.

Comment thread Mathlib/Algebra/Order/Antidiag/Prod.lean
Copyright (c) 2023 Antoine Chambert-Loir and María Inés de Frutos-Fernández. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Antoine Chambert-Loir, María Inés de Frutos-Fernández, Bhavik Mehta, Eric Wieser
Authors: Antoine Chambert-Loir, María Inés de Frutos-Fernández, Bhavik Mehta, Eric Wieser, Fengyang Wang
Copy link
Copy Markdown
Member

@jcommelin jcommelin Feb 18, 2026

Choose a reason for hiding this comment

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

Suggested change
Authors: Antoine Chambert-Loir, María Inés de Frutos-Fernández, Bhavik Mehta, Eric Wieser, Fengyang Wang
Authors: Antoine Chambert-Loir, María Inés de Frutos-Fernández, Bhavik Mehta, Eric Wieser

Is this intentional?
Maybe the name should be added, but this PR wouldn't be the right place.

@jcommelin jcommelin added the awaiting-author A reviewer has asked the author a question or requested changes. label Feb 18, 2026
@mathlib-merge-conflicts mathlib-merge-conflicts bot added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Mar 4, 2026
@mathlib-merge-conflicts
Copy link
Copy Markdown

mathlib-merge-conflicts bot commented Mar 4, 2026

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

@IlPreteRosso IlPreteRosso changed the title refactor(Data.Finset.*Antidiagonal): rename defs to set*Antidiagonal and deprecate old names in namespace Finset refactor(Data.Finset.MulAntidiagonal): rename set-based mulAntidiagonal to setMulAntidiagonal Apr 3, 2026
@IlPreteRosso
Copy link
Copy Markdown
Contributor Author

IlPreteRosso commented Apr 3, 2026

Closing in favor of a fresh PR with the full rename (defs + theorems) as requested in review.

@IlPreteRosso IlPreteRosso mentioned this pull request Apr 3, 2026
Open
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@jcommelin jcommelin jcommelin left review comments

@kim-em kim-em Awaiting requested review from kim-em

Assignees

@jcommelin jcommelin

Labels

awaiting-author A reviewer has asked the author a question or requested changes. merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) new-contributor This PR was made by a contributor with at most 5 merged PRs. Welcome to the community! t-algebra Algebra (groups, rings, fields, etc)

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

4 participants

@IlPreteRosso @Ruben-VandeVelde @kim-em @jcommelin