to_additive on MulZeroClass

Stream: mathlib4

[Christian Merten]

While working with shrinks, I encountered a to_additive failure that I tracked down to docs#Equiv.instMulZeroClassShrink which is tagged with to_additive and produces docs#Equiv.instAddZeroClassShrink (which has identical type signature).

Currently adding to_additive in (docs#Equiv.instMulOneClassShrink)

@[to_additive]
noncomputable instance [Small.{v} α] [MulOneClass α] : MulOneClass (Shrink.{v} α) :=
  (equivShrink α).symm.mulOneClass

yields a warning that the additive declaration already exists. Indeed, it generates the name Equiv.instAddZeroClassShrink which is the non-sensical docs#Equiv.instAddZeroClassShrink.

I suggest to remove the to_additive attribute on docs#Equiv.instMulZeroClassShrink and put it instead on docs#Equiv.instMulOneClassShrink. Do you agree?

(In general I suspect that any to_additive tag on something related to MulZeroClass is wrong).

[Yaël Dillies]

Yeah that just looks like an oversight

[Christian Merten]

#11277