Add Pi.mulSingle_eq_mulIndicator

Stream: PR reviews

[Fengyang Wang]

#34083 (easy)
Add Pi.mulSingle_eq_mulIndicator and Pi.single_eq_indicator (via @[to_additive]), showing that on non-dependent functions:

Pi.mulSingle i x = Set.mulIndicator {i} (fun _ => x)
Pi.single i x = Set.indicator {i} (fun _ => x)

This is the direct Pi analog of Finsupp.single_eq_set_indicator, without involving Finsupp.

[Fengyang Wang]

Quick question how do I change the topic label of a PR?

[Ruben Van de Velde]

I think I would have swapped the left and right hand sides, not sure if anyone else has thoughts

[Fengyang Wang]

Ruben Van de Velde said:

I think I would have swapped the left and right hand sides, not sure if anyone else has thoughts

Yah it makes sense to state a lemma like X_eq_Y where X is more type-native.

[Eric Wieser]

Yeah, I think this should be called mulIndicator_singleton or mulIndicator_singleton_eq_mulSingle or similar

[Eric Wieser]

And we should deprecate and flip the Finsupp lemma to be consistent

[Fengyang Wang]

@Yury G. Kudryashov committed and updated PR title/description

[Yury G. Kudryashov]

Should we generalize it to Set.indicator {i} f = Pi.single i (f i)? Should we make it a simp lemma?

[Fengyang Wang]

Yury G. Kudryashov said:

Should we generalize it to Set.indicator {i} f = Pi.single i (f i)? Should we make it a simp lemma?

Good idea. Updated

Also can make another PR (#34095) about generalizing this in Mathlib.Data.Finsupp.Indicator

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

Ok I'll actually replace this theorem with the more general version as all its use cases are in the same file that declares it

[Fengyang Wang]

@Yury G. Kudryashov Can't mark it with simp, it triggers error due to over simplification in Mathlib.MeasureTheory.Measure.Haar.Unique line 486-487

convert NNReal.tendsto_coe.2 T
simp
^^^

[Yury G. Kudryashov]

This usually means that we miss a simp lemma elsewhere. I'm looking into this.

[Yury G. Kudryashov]

Fixed

[Yury G. Kudryashov]

Sent to the merge queue