Documentation

Mathlib.Algebra.GroupWithZero.TransferInstance

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 β] :

Transfer SemigroupWithZero across an Equiv

Equations
    Instances For
      @[reducible, inline]
      abbrev Equiv.mulZeroClass {α : Type u} {β : Type v} (e : α ≃ β) [MulZeroClass β] :

      Transfer MulZeroClass across an Equiv

      Equations
        Instances For
          @[reducible, inline]
          abbrev Equiv.mulZeroOneClass {α : Type u} {β : Type v} (e : α ≃ β) [MulZeroOneClass β] :

          Transfer MulZeroOneClass across an Equiv

          Equations
            Instances For
              @[reducible, inline]
              abbrev Equiv.monoidWithZero {α : Type u} {β : Type v} (e : α ≃ β) [MonoidWithZero β] :

              Transfer MonoidWithZero across an Equiv

              Equations
                Instances For
                  @[reducible, inline]
                  abbrev Equiv.commMonoidWithZero {α : Type u} {β : Type v} (e : α ≃ β) [CommMonoidWithZero β] :

                  Transfer CommMonoidWithZero across an Equiv

                  Equations
                    Instances For