Documentation

Mathlib.Algebra.Order.Ring.Synonym

Ring structure on the order type synonyms #

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

Order dual #

source
instance instDistribOrderDual {R : Type u_1} [h : Distrib R] :
Distrib Rᵒᵈ
Equations
    source
    instance instLeftDistribClassOrderDual {R : Type u_1} [Mul R] [Add R] [h : LeftDistribClass R] :
    LeftDistribClass Rᵒᵈ
    source
    instance instRightDistribClassOrderDual {R : Type u_1} [Mul R] [Add R] [h : RightDistribClass R] :
    RightDistribClass Rᵒᵈ
    source
    instance instNonUnitalNonAssocSemiringOrderDual {R : Type u_1} [h : NonUnitalNonAssocSemiring R] :
    NonUnitalNonAssocSemiring Rᵒᵈ
    Equations
      source
      instance instNonUnitalSemiringOrderDual {R : Type u_1} [h : NonUnitalSemiring R] :
      NonUnitalSemiring Rᵒᵈ
      Equations
        source
        instance instNonAssocSemiringOrderDual {R : Type u_1} [h : NonAssocSemiring R] :
        NonAssocSemiring Rᵒᵈ
        Equations
          source
          instance instSemiringOrderDual {R : Type u_1} [h : Semiring R] :
          Semiring Rᵒᵈ
          Equations
            source
            instance instNonUnitalCommSemiringOrderDual {R : Type u_1} [h : NonUnitalCommSemiring R] :
            NonUnitalCommSemiring Rᵒᵈ
            Equations
              source
              instance instCommSemiringOrderDual {R : Type u_1} [h : CommSemiring R] :
              CommSemiring Rᵒᵈ
              Equations
                source
                instance instHasDistribNegOrderDual {R : Type u_1} [Mul R] [h : HasDistribNeg R] :
                HasDistribNeg Rᵒᵈ
                Equations
                  source
                  instance instNonUnitalNonAssocRingOrderDual {R : Type u_1} [h : NonUnitalNonAssocRing R] :
                  NonUnitalNonAssocRing Rᵒᵈ
                  Equations
                    source
                    instance instNonUnitalRingOrderDual {R : Type u_1} [h : NonUnitalRing R] :
                    NonUnitalRing Rᵒᵈ
                    Equations
                      source
                      instance instNonAssocRingOrderDual {R : Type u_1} [h : NonAssocRing R] :
                      NonAssocRing Rᵒᵈ
                      Equations
                        source
                        instance instRingOrderDual {R : Type u_1} [h : Ring R] :
                        Ring Rᵒᵈ
                        Equations
                          source
                          instance instNonUnitalCommRingOrderDual {R : Type u_1} [h : NonUnitalCommRing R] :
                          NonUnitalCommRing Rᵒᵈ
                          Equations
                            source
                            instance instCommRingOrderDual {R : Type u_1} [h : CommRing R] :
                            CommRing Rᵒᵈ
                            Equations
                              source
                              instance instIsDomainOrderDual {R : Type u_1} [Ring R] [h : IsDomain R] :
                              IsDomain Rᵒᵈ

                              Lexicographical order #

                              source
                              instance instDistribLex {R : Type u_1} [h : Distrib R] :
                              Distrib (Lex R)
                              Equations
                                source
                                instance instLeftDistribClassLex {R : Type u_1} [Mul R] [Add R] [h : LeftDistribClass R] :
                                LeftDistribClass (Lex R)
                                source
                                instance instRightDistribClassLex {R : Type u_1} [Mul R] [Add R] [h : RightDistribClass R] :
                                RightDistribClass (Lex R)
                                source
                                instance instNonUnitalNonAssocSemiringLex {R : Type u_1} [h : NonUnitalNonAssocSemiring R] :
                                NonUnitalNonAssocSemiring (Lex R)
                                Equations
                                  source
                                  instance instNonUnitalSemiringLex {R : Type u_1} [h : NonUnitalSemiring R] :
                                  NonUnitalSemiring (Lex R)
                                  Equations
                                    source
                                    instance instNonAssocSemiringLex {R : Type u_1} [h : NonAssocSemiring R] :
                                    NonAssocSemiring (Lex R)
                                    Equations
                                      source
                                      instance instSemiringLex {R : Type u_1} [h : Semiring R] :
                                      Semiring (Lex R)
                                      Equations
                                        source
                                        instance instNonUnitalCommSemiringLex {R : Type u_1} [h : NonUnitalCommSemiring R] :
                                        NonUnitalCommSemiring (Lex R)
                                        Equations
                                          source
                                          instance instCommSemiringLex {R : Type u_1} [h : CommSemiring R] :
                                          CommSemiring (Lex R)
                                          Equations
                                            source
                                            instance instHasDistribNegLex {R : Type u_1} [Mul R] [h : HasDistribNeg R] :
                                            HasDistribNeg (Lex R)
                                            Equations
                                              source
                                              instance instNonUnitalNonAssocRingLex {R : Type u_1} [h : NonUnitalNonAssocRing R] :
                                              NonUnitalNonAssocRing (Lex R)
                                              Equations
                                                source
                                                instance instNonUnitalRingLex {R : Type u_1} [h : NonUnitalRing R] :
                                                NonUnitalRing (Lex R)
                                                Equations
                                                  source
                                                  instance instNonAssocRingLex {R : Type u_1} [h : NonAssocRing R] :
                                                  NonAssocRing (Lex R)
                                                  Equations
                                                    source
                                                    instance instRingLex {R : Type u_1} [h : Ring R] :
                                                    Ring (Lex R)
                                                    Equations
                                                      source
                                                      instance instNonUnitalCommRingLex {R : Type u_1} [h : NonUnitalCommRing R] :
                                                      NonUnitalCommRing (Lex R)
                                                      Equations
                                                        source
                                                        instance instCommRingLex {R : Type u_1} [h : CommRing R] :
                                                        CommRing (Lex R)
                                                        Equations
                                                          source
                                                          instance instIsDomainLex {R : Type u_1} [Ring R] [h : IsDomain R] :
                                                          IsDomain (Lex R)