quo vadis `pi.single`

Stream: general

[Joachim Breitner]

Currently, we have pi.single for the function that is 0 everywhere but at one index. When working with pi-groups, we also need a variant that is 1 everywhere. The two can be provided together using the @[to_additive] machinery. But how should we name them?

[Joachim Breitner]

/poll Names for pi.single variants
rename to pi.add_single, usepi.single for the multiplicative variant
keep pi.add_single, addpi.mul_single for
use pi.single₀ and pi.single₁

[Joachim Breitner]

“keep pi.add_single” was of course a confusing typo, ignore that option :-)

[Eric Wieser]

This of course also inevitably extends to finsupp / mul_finsupp, dfinsupp / mul_dfinsupp, ...

[Yaël Dillies]

That's what I keep saying :wink:

[Yaël Dillies]

cf https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/multiplicative.20finsupp