Transfer algebraic structures across Equivs

This continues the pattern set in Mathlib/Algebra/Group/TransferInstance.lean.

@[reducible, inline]

abbrev Equiv.smulZeroClass (M : Type u_1) {A : Type u_3} {B : Type u_4} (e : A ≃ B) [Zero B] [SMulZeroClass M B] : SMulZeroClass M A

Transfer SMulZeroClass across an Equiv

@[reducible, inline]

abbrev Equiv.smulWithZero (M₀ : Type u_2) {A : Type u_3} {B : Type u_4} (e : A ≃ B) [Zero M₀] [Zero B] [SMulWithZero M₀ B] : SMulWithZero M₀ A

Transfer SMulWithZero across an Equiv

@[reducible, inline]

abbrev Equiv.mulActionWithZero (M₀ : Type u_2) {A : Type u_3} {B : Type u_4} (e : A ≃ B) [MonoidWithZero M₀] [Zero B] [MulActionWithZero M₀ B] : MulActionWithZero M₀ A

Transfer MulActionWithZero across an Equiv

@[reducible, inline]

abbrev Equiv.distribSMul (M : Type u_1) {A : Type u_3} {B : Type u_4} (e : A ≃ B) [AddZeroClass B] [DistribSMul M B] : DistribSMul M A

Transfer DistribSMul across an Equiv

@[reducible, inline]

abbrev Equiv.distribMulAction (M : Type u_1) {A : Type u_3} {B : Type u_4} (e : A ≃ B) [Monoid M] [AddMonoid B] [DistribMulAction M B] : DistribMulAction M A

Transfer DistribMulAction across an Equiv