Transfer algebraic structures across Equivs

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

@[reducible, inline]

abbrev Equiv.semigroupWithZero {α : Type u} {β : Type v} (e : α ≃ β) [SemigroupWithZero β] : SemigroupWithZero α

Transfer SemigroupWithZero across an Equiv

Equations

• e.semigroupWithZero = Function.Injective.semigroupWithZero ⇑e ⋯ ⋯ ⋯

@[reducible, inline]

abbrev Equiv.mulZeroClass {α : Type u} {β : Type v} (e : α ≃ β) [MulZeroClass β] : MulZeroClass α

Transfer MulZeroClass across an Equiv

Equations

• e.mulZeroClass = Function.Injective.mulZeroClass ⇑e ⋯ ⋯ ⋯

@[reducible, inline]

abbrev Equiv.mulZeroOneClass {α : Type u} {β : Type v} (e : α ≃ β) [MulZeroOneClass β] : MulZeroOneClass α

Transfer MulZeroOneClass across an Equiv

Equations

• e.mulZeroOneClass = Function.Injective.mulZeroOneClass ⇑e ⋯ ⋯ ⋯ ⋯

@[reducible, inline]

abbrev Equiv.distribMulAction {α : Type u} {β : Type v} (M : Type u_1) [Monoid M] (e : α ≃ β) [AddCommMonoid β] [DistribMulAction M β] : DistribMulAction M α

Transfer DistribMulAction across an Equiv

Equations

• Equiv.distribMulAction M e = { toMulAction := Equiv.mulAction M e, smul_zero := ⋯, smul_add := ⋯ }