Pi.single

Stream: mathlib4

[Violeta Hernández]

Is there any reason why docs#Finsupp.single_eq_pi_single isn't a simp lemma? And what's up with lemmas such as docs#Finsupp.single_eq_set_indicator ? Is this an oversight, or a design decision?

[Alfredo Moreira-Rosa]

My guess is because it's usually a bad idea to unfold, if simp was making it pi single, you are now forced to prove everything at this level ?

[Yury G. Kudryashov]

This lemma was added much later than API for Finsupp.single was established. I think that we should make it a simp lemma, deprecate all lemmas about Finsupp.single_apply*, and generalize those that are still relevant to Pi.single.

[Violeta Hernández]

ok so, trying to do this change I ended up answering my own question

[Violeta Hernández]

Pi.single takes a DecidableEq argument, Finsupp.single does not

[Eric Wieser]

I have a PR somewhere that tries to change Finsupp not to omit that argument

[Eric Wieser]

But this is a huge can of worms that would do better to wait until @Yaël Dillies' MonoidAlgebra refactor goes through

[Violeta Hernández]

Is there an open PR for that?

[Eric Wieser]

#30877 is the next piece