Commit 2026-01-20 16:34 9acd28ad

feat(Data/Finsupp/Single): generalize single_eq_set_indicator (#34095) Generalize Finsupp.single_eq_set_indicator to arbitrary functions, with the old statement available as single_eq_set_indicator':

theorem single_eq_set_indicator (a : α) (f : α → M) :
    ⇑(single a (f a)) = Set.indicator {a} f