refactor(Data/Finsupp): deprecate direct single ↔ Set.indicator shortcuts, add indicator_eq_set_indicator by IlPreteRosso · Pull Request #34182 · leanprover-community/mathlib4

IlPreteRosso · 2026-01-20T21:59:59Z

Routes Finsupp.single ↔ Set.indicator through Pi.single instead of direct shortcuts.

Adds indicator_eq_set_indicator bridging Finsupp.indicator and Set.indicator for non-dependent functions. Deprecates single_eq_set_indicator and single_eq_indicator — users should compose through single_eq_pi_single + Set.indicator_singleton instead. Golfs single_eq_update via single_eq_pi_single.

Continues #34083.

github-actions · 2026-01-20T22:01:08Z

PR summary cd8272a9d5

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.Data.Finsupp.Single	439	447	+8 (+1.82%)
Mathlib.Data.Finsupp.Indicator	440	448	+8 (+1.82%)

Import changes for all files

Files	Import difference
33 files `Mathlib.Algebra.BigOperators.Associated` `Mathlib.Algebra.BigOperators.Finsupp.Basic` `Mathlib.Algebra.BigOperators.Finsupp.Fin` `Mathlib.Algebra.FreeAbelianGroup.Finsupp` `Mathlib.Algebra.FreeAbelianGroup.UniqueSums` `Mathlib.Algebra.FreeMonoid.UniqueProds` `Mathlib.Algebra.Group.Finsupp` `Mathlib.Algebra.Group.Subgroup.Finsupp` `Mathlib.Algebra.Group.Submonoid.Finsupp` `Mathlib.Algebra.Group.UniqueProds.Basic` `Mathlib.Algebra.GroupWithZero.Torsion` `Mathlib.Algebra.Order.Antidiag.Finsupp` `Mathlib.Algebra.Order.Floor.Div` `Mathlib.Algebra.Star.BigOperators` `Mathlib.Combinatorics.Enumerative.Partition.Basic` `Mathlib.Combinatorics.Enumerative.Partition` `Mathlib.Data.DFinsupp.Notation` `Mathlib.Data.Finset.Finsupp` `Mathlib.Data.Finsupp.BigOperators` `Mathlib.Data.Finsupp.Ext` `Mathlib.Data.Finsupp.NeLocus` `Mathlib.Data.Finsupp.Pointwise` `Mathlib.Data.Finsupp.SMulWithZero` `Mathlib.Data.List.ToFinsupp` `Mathlib.Data.ZMod.Units` `Mathlib.RingTheory.Localization.NumDen` `Mathlib.RingTheory.UniqueFactorizationDomain.Basic` `Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet` `Mathlib.RingTheory.UniqueFactorizationDomain.Finite` `Mathlib.RingTheory.UniqueFactorizationDomain.GCDMonoid` `Mathlib.RingTheory.UniqueFactorizationDomain.Multiplicative` `Mathlib.RingTheory.UniqueFactorizationDomain.Nat` `Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors`	1
`Mathlib.Data.Finsupp.Fintype`	2
4 files `Mathlib.Data.Finsupp.Fin` `Mathlib.Data.Finsupp.Indicator` `Mathlib.Data.Finsupp.Notation` `Mathlib.Data.Finsupp.Single`	8

Declarations diff

+ indicator_eq_set_indicator
+ indicator_singleton
+ set_indicator_singleton
- Set.indicator_singleton_eq

You can run this locally as follows

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

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

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

No changes to technical debt.

You can run this locally as

./scripts/reporting/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).

eric-wieser

Please update the PR title; this commit does not add anything, it just golfs!

bors d+

mathlib-bors · 2026-01-20T22:56:39Z

✌️ IlPreteRosso can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

eric-wieser · 2026-01-20T22:57:10Z

bors d-

mathlib-bors · 2026-01-20T22:57:13Z

🚫 All delegations have been removed from this PR. To re-add a delegation, reply with bors d+ (to delegate the PR author) or bors d=list,of,github,usernames to delegate multiple users.

See above

IlPreteRosso · 2026-01-21T03:22:11Z

@eric-wieser We have

theorem mulIndicator_singleton (i : ι) (f : ι → M) :
    Set.mulIndicator {i} f = Pi.mulSingle i (f i) := by

in Mathlib.Algebra.Group.Indicator, with @[to_additive]. In fact this was added to Mathlib by my previous PR #34083

We don't have the coe version of this in Mathlib.Data.Finsupp.Single, only the one specialized to constant function.

For this PR I wanted to add this coe statement in Finsupp.

…leton_indicator_eq to Mathlib.Data.Finsupp.Single

IlPreteRosso · 2026-01-21T03:49:50Z

@eric-wieser I added all the versions in question please let me know which one we want and in what direction, I'm a bit confused by the similar theorem names and files.

One thing is that single_eq_set_indicator is originally in Mathlib, and needs generalization. For the directions I just followed the context.

My intention was simple, I saw theorems A c = B c taking in a constant function c, I stated A f = B f, for general f, in the same direction and in the same namespace, with the same type signature, and then golfed the constant version using the general version.

…ngle.lean and Indicator.lean

…export

eric-wieser · 2026-01-21T05:04:40Z

    Set.indicator {a} f = ⇑(single a (f a)) := by
  classical
  ext x
  simp only [Set.indicator, Set.mem_singleton_iff, single_apply, @eq_comm _ a]
  split_ifs with h <;> simp [h]


This has a much shorter proof which I think is classical rw [Set.indicator_singleton, Finsupp.single_eq_pi_single].

Set.indicator_singleton changes import Mathlib.Algebra.Notation.Indicator to import Mathlib.Algebra.Group.Indicator, need to move single_eq_pi_single to before set_indicator_singleton within Single.lean. Then set_indicator_singleton is golfed. Also golfed the relocated single_eq_pi_single.

eric-wieser · 2026-01-21T05:09:18Z

In fact this was added to Mathlib by my previous PR #34083

Sorry about this, indeed the lemma I was asking for is already there!

One thing is that single_eq_set_indicator is originally in Mathlib, and needs generalization. For the directions I just followed the context.

I would actually lean towards deprecating it, and making the user rewrite through Finsupp.single_eq_pi_single then Set.indicator_singleton, or via Finsupp.indicator_singleton followed by a seemingly missing lemma linking Finsupp.indicator and Set.indicator.

Generally I would think of theorems as filling out the edges of a hypercube, not as also filling every possible diagonal.

eric-wieser · 2026-01-21T05:09:41Z

Let's see what @urkud thinks

IlPreteRosso · 2026-01-21T05:16:40Z

@eric-wieser No worries! I'll wait for more input then. Also as my earlier reply

Set.indicator_singleton changes import

Now bot added large-import warning. So a trade off between golf and import.

Generally I would think of theorems as filling out the edges of a hypercube, not as also filling every possible diagonal.

I like this way of thinking.

IlPreteRosso · 2026-01-25T20:16:57Z

@urkud Sorry to tag you again, just in case you missed the previous tag

urkud · 2026-01-30T14:52:52Z

I'm sorry for the delay. I'll look into this over the weekend.

IlPreteRosso · 2026-02-06T16:45:22Z

Hi @urkud, sorry to tag you again, just would like to remind you that here's still a PR awaiting your review.

…ndicator_eq_set_indicator` theorem

github-actions · 2026-04-03T17:10:47Z

✅ PR Title Formatted Correctly

The title of this PR has been updated to match our commit style conventions.
Thank you!

IlPreteRosso · 2026-04-03T17:15:10Z

@eric-wieser Updated per your suggestion — single_eq_set_indicator and single_eq_indicator are now deprecated, routing through Pi.single instead. Also added the missing indicator_eq_set_indicator bridge between Finsupp.indicator and Set.indicator.

IlPreteRosso and others added 5 commits January 17, 2026 23:56

single_eq_set_indicator'

865541b

swap two versions

77fee65

Set.indicator_singleton_eq

5a7e709

Merge branch 'leanprover-community:master' into FinsuppSingle

612f796

missing update from leanprover-community#34095

c76e48c

github-actions bot added the new-contributor This PR was made by a contributor with at most 5 merged PRs. Welcome to the community! label Jan 20, 2026

IlPreteRosso mentioned this pull request Jan 20, 2026

[Merged by Bors] - feat(Data/Finsupp/Single): generalize single_eq_set_indicator #34095

Closed

github-actions bot added t-data Data (lists, quotients, numbers, etc) easy < 20s of review time. See the lifecycle page for guidelines. labels Jan 20, 2026

eric-wieser previously approved these changes Jan 20, 2026

View reviewed changes

ghost added the delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). label Jan 20, 2026

ghost removed the delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). label Jan 20, 2026

eric-wieser reviewed Jan 20, 2026

View reviewed changes

Comment thread Mathlib/Data/Finsupp/Single.lean Outdated

eric-wieser added the awaiting-author A reviewer has asked the author a question or requested changes. label Jan 21, 2026

rename

cfcc494

eric-wieser reviewed Jan 21, 2026

View reviewed changes

Comment thread Mathlib/Data/Finsupp/Single.lean Outdated

IlPreteRosso added 2 commits January 20, 2026 22:40

indicator_singleton in Mathlib.Data.Finsupp.Indicator

b45084d

add single_indicator_eq in Mathlib.Data.Finsupp.Single, add back sing…

12b3f48

…leton_indicator_eq to Mathlib.Data.Finsupp.Single

github-actions bot added WIP Work in progress and removed awaiting-author A reviewer has asked the author a question or requested changes. labels Jan 21, 2026

eric-wieser reviewed Jan 21, 2026

View reviewed changes

Comment thread Mathlib/Data/Finsupp/Indicator.lean Outdated

IlPreteRosso added 2 commits January 20, 2026 23:00

rename and flip single_indicator_eq to indicator_singleton in both Si…

df59888

…ngle.lean and Indicator.lean

Resolve collision of Finsupp.indicator_singleton which the two files …

365c6cb

…export

IlPreteRosso changed the title ~~feat(Data/Finsupp/Single): add Set.indicator_singleton_eq~~ feat(Data/Finsupp/Single, Data/Finsupp/Indicator): Add set_indicator_singleton, indicator_singleton; golfed single_eq_set_indicator, single_eq_indicator Jan 21, 2026

eric-wieser reviewed Jan 21, 2026

View reviewed changes

Comment thread Mathlib/Data/Finsupp/Indicator.lean

eric-wieser reviewed Jan 21, 2026

View reviewed changes

some refactor and golf

06fc9a9

github-actions bot added the large-import Automatically added label for PRs with a significant increase in transitive imports label Jan 21, 2026

ocfnash removed the easy < 20s of review time. See the lifecycle page for guidelines. label Jan 21, 2026

leanprover-community-bot-assistant assigned joneugster Jan 26, 2026

joneugster assigned urkud and eric-wieser and unassigned joneugster Jan 30, 2026

mathlib-triage bot assigned TwoFX and unassigned eric-wieser and urkud Mar 22, 2026

Merge branch 'leanprover-community:master' into FinsuppSingle

181675f

github-actions bot removed the large-import Automatically added label for PRs with a significant increase in transitive imports label Apr 3, 2026

IlPreteRosso added 2 commits April 3, 2026 13:03

Deprecate indicator_singleton and set_indicator_singleton, add `i…

9a2cfa8

…ndicator_eq_set_indicator` theorem

Merge remote FinsuppSingle

69b31e9

IlPreteRosso changed the title ~~feat/deprecation(Data/Finsupp): add indicator_eq_set_indicator, deprecate single_eq_set_indicator and single_eq_indicator~~ feat/deprecation(Data/Finsupp): add indicator_eq_set_indicator, deprecate direct Finsupp.single ↔ Set.indicator shortcuts Apr 3, 2026

IlPreteRosso changed the title ~~feat/deprecation(Data/Finsupp): add indicator_eq_set_indicator, deprecate direct Finsupp.single ↔ Set.indicator shortcuts~~ refactor(Data/Finsupp): deprecate direct single ↔ Set.indicator shortcuts, add indicator_eq_set_indicator Apr 3, 2026

IlPreteRosso added 2 commits April 3, 2026 13:18

warning

0443ed0

deprecation calls

3b2500b

Conversation

IlPreteRosso commented Jan 20, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

github-actions bot commented Jan 20, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

PR summary cd8272a9d5

Import changes for modified files

Declarations diff

Uh oh!

eric-wieser left a comment

Choose a reason for hiding this comment

Uh oh!

mathlib-bors bot commented Jan 20, 2026

Uh oh!

eric-wieser commented Jan 20, 2026

Uh oh!

mathlib-bors bot commented Jan 20, 2026

Uh oh!

Uh oh!

Uh oh!

IlPreteRosso commented Jan 21, 2026

Uh oh!

IlPreteRosso commented Jan 21, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

Uh oh!

Uh oh!

eric-wieser Jan 21, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

IlPreteRosso Jan 21, 2026

Choose a reason for hiding this comment

Uh oh!

eric-wieser commented Jan 21, 2026

Uh oh!

eric-wieser commented Jan 21, 2026

Uh oh!

IlPreteRosso commented Jan 21, 2026

Uh oh!

IlPreteRosso commented Jan 25, 2026

Uh oh!

urkud commented Jan 30, 2026

Uh oh!

IlPreteRosso commented Feb 6, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

github-actions bot commented Apr 3, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

✅ PR Title Formatted Correctly

Uh oh!

IlPreteRosso commented Apr 3, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

6 participants

IlPreteRosso commented Jan 20, 2026 •

edited

Loading

github-actions bot commented Jan 20, 2026 •

edited

Loading

IlPreteRosso commented Jan 21, 2026 •

edited

Loading

eric-wieser Jan 21, 2026 •

edited

Loading

IlPreteRosso commented Feb 6, 2026 •

edited

Loading

github-actions bot commented Apr 3, 2026 •

edited

Loading