Should `Pi.instHSMul` exist in Mathlib?

Stream: mathlib4

[Alex Kontorovich]

Continuing discussion from here.

Is there a reason not to add Pi.instHSMul as an analogue to Pi.instSMul? Thanks!

[Eric Wieser]

I think I've argued in the past that such actions are almost guaranteed to create diamonds

[Eric Wieser]

Indeed, section 4.8 of my thesis has a diagram

(I guess strictly that's HMul not HSMul, but I don't think the difference matters)

[Notification Bot]

2 messages were moved here from #Is there code for X? > smul inferred by function instance by Eric Wieser.