pi.single but for multiplicative groups

Stream: Is there code for X?

[Joachim Breitner]

There is pi.single with type (i : I) : f i → Π i, f i, but it works with has_zero. Is there an equivalent when working with multiplicative groups? Should I add it? (pi.single1?) Or just use function.update 1 i x in my development?

[Johan Commelin]

I think that either of those is fine.