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

Equations

• Equiv.smulZeroClass M e = { 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 B] [SMulWithZero M₀ B] : SMulWithZero M₀ A

Transfer SMulWithZero across an Equiv

Equations

• Equiv.smulWithZero M₀ e = { toSMulZeroClass := Equiv.smulZeroClass M₀ e, 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 B] [MulActionWithZero M₀ B] : MulActionWithZero M₀ A

Transfer MulActionWithZero across an Equiv

Equations

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

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

Equations

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

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

Equations

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