Commit 2026-04-27 20:25 263b57bb

View on Github →

refactor(Data/Finsupp): deprecate direct single ↔ Set.indicator shortcuts, add indicator_eq_set_indicator (#34182) deprecates single_eq_set_indicator and single_eq_indicator, routing through Pi.single instead. Also added the missing indicator_eq_set_indicator bridge between Finsupp.indicator and Set.indicator. Continues #34083.

Estimated changes

Modified Mathlib/Data/Finsupp/Indicator.lean

added theorem Finsupp.indicator_eq_set_indicator

added theorem Finsupp.indicator_singleton

modified theorem Finsupp.single_eq_indicator

Modified Mathlib/Data/Finsupp/Single.lean

deleted theorem Finsupp.Set.indicator_singleton_eq

added theorem Finsupp.set_indicator_singleton

modified theorem Finsupp.single_eq_pi_single

modified theorem Finsupp.single_eq_set_indicator