Transfer algebraic structures across Equivs or AddEquivs

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 A] [Zero B] [SMulZeroClass M B] (map_zero : e 0 = 0) : 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 A] [Zero B] [SMulWithZero M₀ B] (map_zero : e 0 = 0) : 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 A] [Zero B] [MulActionWithZero M₀ B] (map_zero : e 0 = 0) : MulActionWithZero M₀ A

Transfer MulActionWithZero across an Equiv

@[reducible, inline]

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

Transfer DistribSMul across an AddEquiv

@[reducible, inline]

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

Transfer DistribMulAction across an AddEquiv

@[deprecated AddEquiv.distribSMul (since := "2026-07-30")]

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

Alias of AddEquiv.distribSMul.

---

Transfer DistribSMul across an AddEquiv

@[deprecated AddEquiv.distribMulAction (since := "2026-07-30")]

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

Alias of AddEquiv.distribMulAction.

---

Transfer DistribMulAction across an AddEquiv