Transfer group with zero structures from α to Shrink α

@[instance_reducible]

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

Equations

• instSemigroupWithZeroShrink = { toSemigroup := Shrink.instSemigroup, toZero := Shrink.instZero, zero_mul := ⋯, mul_zero := ⋯ }

@[instance_reducible]

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

Equations

• instMulZeroClassShrink = { toMul := Shrink.instMul, toZero := Shrink.instZero, zero_mul := ⋯, mul_zero := ⋯ }

@[instance_reducible]

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

Equations

• instMulZeroOneClassShrink = { toMulOneClass := Shrink.instMulOneClass, toZero := Shrink.instZero, zero_mul := ⋯, mul_zero := ⋯ }

@[instance_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 = { toMulAction := Shrink.instMulAction, smul_zero := ⋯, smul_add := ⋯ }