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.monoidWithZero {α : Type u} {β : Type v} (e : α ≃ β) [MonoidWithZero β] : MonoidWithZero α

Transfer MonoidWithZero across an Equiv

Equations

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

@[reducible, inline]

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

Transfer CommMonoidWithZero across an Equiv

Equations

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