Documentation

Mathlib.Algebra.GroupWithZero.Opposite

Opposites of groups with zero #

source
instance MulOpposite.instMulZeroClass {α : Type u_1} [MulZeroClass α] :
MulZeroClass αᵐᵒᵖ
Equations
    source
    instance MulOpposite.instMulZeroOneClass {α : Type u_1} [MulZeroOneClass α] :
    MulZeroOneClass αᵐᵒᵖ
    Equations
      source
      instance MulOpposite.instSemigroupWithZero {α : Type u_1} [SemigroupWithZero α] :
      SemigroupWithZero αᵐᵒᵖ
      Equations
        source
        instance MulOpposite.instMonoidWithZero {α : Type u_1} [MonoidWithZero α] :
        MonoidWithZero αᵐᵒᵖ
        Equations
          source
          instance MulOpposite.instGroupWithZero {α : Type u_1} [GroupWithZero α] :
          GroupWithZero αᵐᵒᵖ
          Equations
            source
            instance MulOpposite.instNoZeroDivisors {α : Type u_1} [Zero α] [Mul α] [NoZeroDivisors α] :
            NoZeroDivisors αᵐᵒᵖ
            source
            instance MulOpposite.instIsRightCancelMulZeroOfIsLeftCancelMulZero {α : Type u_1} [Mul α] [Zero α] [IsLeftCancelMulZero α] :
            IsRightCancelMulZero αᵐᵒᵖ
            source
            instance MulOpposite.instIsLeftCancelMulZeroOfIsRightCancelMulZero {α : Type u_1} [Mul α] [Zero α] [IsRightCancelMulZero α] :
            IsLeftCancelMulZero αᵐᵒᵖ
            source
            instance MulOpposite.instIsCancelMulZero {α : Type u_1} [Mul α] [Zero α] [IsCancelMulZero α] :
            IsCancelMulZero αᵐᵒᵖ
            source
            @[simp]
            theorem MulOpposite.isLeftCancelMulZero_iff {α : Type u_1} [Mul α] [Zero α] :
            IsLeftCancelMulZero αᵐᵒᵖ ↔ IsRightCancelMulZero α
            source
            @[simp]
            theorem MulOpposite.isRightCancelMulZero_iff {α : Type u_1} [Mul α] [Zero α] :
            IsRightCancelMulZero αᵐᵒᵖ ↔ IsLeftCancelMulZero α
            source
            @[simp]
            theorem MulOpposite.isCancelMulZero_iff {α : Type u_1} [Mul α] [Zero α] :
            IsCancelMulZero αᵐᵒᵖ ↔ IsCancelMulZero α
            source
            instance AddOpposite.instMulZeroClass {α : Type u_1} [MulZeroClass α] :
            MulZeroClass αᵃᵒᵖ
            Equations
              source
              instance AddOpposite.instMulZeroOneClass {α : Type u_1} [MulZeroOneClass α] :
              MulZeroOneClass αᵃᵒᵖ
              Equations
                source
                instance AddOpposite.instSemigroupWithZero {α : Type u_1} [SemigroupWithZero α] :
                SemigroupWithZero αᵃᵒᵖ
                Equations
                  source
                  instance AddOpposite.instMonoidWithZero {α : Type u_1} [MonoidWithZero α] :
                  MonoidWithZero αᵃᵒᵖ
                  Equations
                    source
                    instance AddOpposite.instNoZeroDivisors {α : Type u_1} [Zero α] [Mul α] [NoZeroDivisors α] :
                    NoZeroDivisors αᵃᵒᵖ
                    source
                    instance AddOpposite.instGroupWithZero {α : Type u_1} [GroupWithZero α] :
                    GroupWithZero αᵃᵒᵖ
                    Equations