Documentation

Mathlib.Algebra.Order.GroupWithZero.Synonym

Group with zero structure on the order type synonyms #

Transfer algebraic instances from α to αᵒᵈ and Lex α.

Order dual #

source
instance instMulZeroClassOrderDual {α : Type u_1} [h : MulZeroClass α] :
MulZeroClass αᵒᵈ
Equations
    source
    instance instMulZeroOneClassOrderDual {α : Type u_1} [h : MulZeroOneClass α] :
    MulZeroOneClass αᵒᵈ
    Equations
      source
      instance instNoZeroDivisorsOrderDual {α : Type u_1} [Mul α] [Zero α] [h : NoZeroDivisors α] :
      NoZeroDivisors αᵒᵈ
      source
      instance instSemigroupWithZeroOrderDual {α : Type u_1} [h : SemigroupWithZero α] :
      SemigroupWithZero αᵒᵈ
      Equations
        source
        instance instMonoidWithZeroOrderDual {α : Type u_1} [h : MonoidWithZero α] :
        MonoidWithZero αᵒᵈ
        Equations
          source
          instance instCancelMonoidWithZeroOrderDual {α : Type u_1} [h : CancelMonoidWithZero α] :
          CancelMonoidWithZero αᵒᵈ
          Equations
            source
            instance instCommMonoidWithZeroOrderDual {α : Type u_1} [h : CommMonoidWithZero α] :
            CommMonoidWithZero αᵒᵈ
            Equations
              source
              instance instCancelCommMonoidWithZeroOrderDual {α : Type u_1} [h : CancelCommMonoidWithZero α] :
              CancelCommMonoidWithZero αᵒᵈ
              Equations
                source
                instance instGroupWithZeroOrderDual {α : Type u_1} [h : GroupWithZero α] :
                GroupWithZero αᵒᵈ
                Equations
                  source
                  instance instCommGroupWithZeroOrderDual {α : Type u_1} [h : CommGroupWithZero α] :
                  CommGroupWithZero αᵒᵈ
                  Equations

                    Lexicographic order #

                    source
                    instance instMulZeroClassLex {α : Type u_1} [h : MulZeroClass α] :
                    MulZeroClass (Lex α)
                    Equations
                      source
                      instance instMulZeroOneClassLex {α : Type u_1} [h : MulZeroOneClass α] :
                      MulZeroOneClass (Lex α)
                      Equations
                        source
                        instance instNoZeroDivisorsLex {α : Type u_1} [Mul α] [Zero α] [h : NoZeroDivisors α] :
                        NoZeroDivisors (Lex α)
                        source
                        instance instSemigroupWithZeroLex {α : Type u_1} [h : SemigroupWithZero α] :
                        SemigroupWithZero (Lex α)
                        Equations
                          source
                          instance instMonoidWithZeroLex {α : Type u_1} [h : MonoidWithZero α] :
                          MonoidWithZero (Lex α)
                          Equations
                            source
                            instance instCancelMonoidWithZeroLex {α : Type u_1} [h : CancelMonoidWithZero α] :
                            CancelMonoidWithZero (Lex α)
                            Equations
                              source
                              instance instCommMonoidWithZeroLex {α : Type u_1} [h : CommMonoidWithZero α] :
                              CommMonoidWithZero (Lex α)
                              Equations
                                source
                                instance instCancelCommMonoidWithZeroLex {α : Type u_1} [h : CancelCommMonoidWithZero α] :
                                CancelCommMonoidWithZero (Lex α)
                                Equations
                                  source
                                  instance instGroupWithZeroLex {α : Type u_1} [h : GroupWithZero α] :
                                  GroupWithZero (Lex α)
                                  Equations
                                    source
                                    instance instCommGroupWithZeroLex {α : Type u_1} [h : CommGroupWithZero α] :
                                    CommGroupWithZero (Lex α)
                                    Equations