Transfer group with zero structures from α to Shrink α

@[implicit_reducible]

noncomputable instance instSemigroupWithZeroShrink {α : Type u_2} [Small.{v, u_2} α] [SemigroupWithZero α] : SemigroupWithZero (Shrink.{v, u_2} α)

Equations

• instSemigroupWithZeroShrink = (equivShrink α).symm.semigroupWithZero

@[implicit_reducible]

noncomputable instance instMulZeroClassShrink {α : Type u_2} [Small.{v, u_2} α] [MulZeroClass α] : MulZeroClass (Shrink.{v, u_2} α)

Equations

• instMulZeroClassShrink = (equivShrink α).symm.mulZeroClass

@[implicit_reducible]

noncomputable instance instMulZeroOneClassShrink {α : Type u_2} [Small.{v, u_2} α] [MulZeroOneClass α] : MulZeroOneClass (Shrink.{v, u_2} α)

Equations

• instMulZeroOneClassShrink = (equivShrink α).symm.mulZeroOneClass

@[implicit_reducible]

noncomputable instance instDistribMulActionShrink {M : Type u_1} {α : Type u_2} [Small.{v, u_2} α] [Monoid M] [AddCommMonoid α] [DistribMulAction M α] : DistribMulAction M (Shrink.{v, u_2} α)

Equations

• instDistribMulActionShrink = Equiv.distribMulAction M (equivShrink α).symm