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

Equations

• Equiv.smulZeroClass M e map_zero = { toSMul := Equiv.smul M e, smul_zero := ⋯ }

@[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

Equations

• Equiv.smulWithZero M₀ e map_zero = { toSMulZeroClass := Equiv.smulZeroClass M₀ e map_zero, zero_smul := ⋯ }

@[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

Equations

• Equiv.mulActionWithZero M₀ e map_zero = { toSMul := (Equiv.smulWithZero M₀ e map_zero).toSMul, mul_smul := ⋯, one_smul := ⋯, smul_zero := ⋯, zero_smul := ⋯ }

@[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

Equations

• AddEquiv.distribSMul M e = { toSMulZeroClass := Equiv.smulZeroClass M e.toEquiv ⋯, smul_add := ⋯ }

@[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

Equations

• AddEquiv.distribMulAction M e = { toSMul := (AddEquiv.distribSMul M e).toSMul, mul_smul := ⋯, one_smul := ⋯, smul_zero := ⋯, smul_add := ⋯ }

@[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

Equations

• Equiv.distribSMul = AddEquiv.distribSMul

@[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

Equations

• Equiv.distribMulAction = AddEquiv.distribMulAction