Zulip Chat Archive

Stream: general

Topic: quo vadis `pi.single`


Joachim Breitner (Feb 05 2022 at 13:47):

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 (Feb 05 2022 at 13:47):

/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 (Feb 05 2022 at 14:04):

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

Eric Wieser (Feb 05 2022 at 15:08):

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

Yaël Dillies (Feb 05 2022 at 15:12):

That's what I keep saying :wink:

Yaël Dillies (Feb 05 2022 at 15:15):

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


Last updated: Dec 20 2023 at 11:08 UTC