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
@[implicit_reducible]
instance OrderDual.instDistrib {R : Type u_1} [Distrib R] :
Distrib Rᵒᵈ
source
instance OrderDual.instLeftDistribClass {R : Type u_1} [Mul R] [Add R] [LeftDistribClass R] :
LeftDistribClass Rᵒᵈ
source
instance OrderDual.instRightDistribClass {R : Type u_1} [Mul R] [Add R] [RightDistribClass R] :
RightDistribClass Rᵒᵈ
source
@[implicit_reducible]
instance OrderDual.instNonUnitalNonAssocSemiring {R : Type u_1} [NonUnitalNonAssocSemiring R] :
NonUnitalNonAssocSemiring Rᵒᵈ
source
@[implicit_reducible]
instance OrderDual.instNatCast {R : Type u_1} [NatCast R] :
NatCast Rᵒᵈ
source
@[implicit_reducible]
instance OrderDual.instIntCast {R : Type u_1} [IntCast R] :
IntCast Rᵒᵈ
source
@[implicit_reducible]
instance OrderDual.instAddMonoidWithOne {R : Type u_1} [AddMonoidWithOne R] :
AddMonoidWithOne Rᵒᵈ
source
@[implicit_reducible]
instance OrderDual.instAddCommMonoidWithOne {R : Type u_1} [AddCommMonoidWithOne R] :
AddCommMonoidWithOne Rᵒᵈ
source
@[implicit_reducible]
instance OrderDual.instAddGroupWithOne {R : Type u_1} [AddGroupWithOne R] :
AddGroupWithOne Rᵒᵈ
source
@[implicit_reducible]
instance OrderDual.instAddCommGroupWithOne {R : Type u_1} [AddCommGroupWithOne R] :
AddCommGroupWithOne Rᵒᵈ
source
@[implicit_reducible]
instance OrderDual.instNonUnitalSemiring {R : Type u_1} [NonUnitalSemiring R] :
NonUnitalSemiring Rᵒᵈ
source
@[implicit_reducible]
instance OrderDual.instNonAssocSemiring {R : Type u_1} [NonAssocSemiring R] :
NonAssocSemiring Rᵒᵈ
source
@[implicit_reducible]
instance OrderDual.instSemiring {R : Type u_1} [Semiring R] :
Semiring Rᵒᵈ
source
@[implicit_reducible]
instance OrderDual.instNonUnitalCommSemiring {R : Type u_1} [NonUnitalCommSemiring R] :
NonUnitalCommSemiring Rᵒᵈ
source
@[implicit_reducible]
instance OrderDual.instCommSemiring {R : Type u_1} [CommSemiring R] :
CommSemiring Rᵒᵈ
source
@[implicit_reducible]
instance OrderDual.instHasDistribNeg {R : Type u_1} [Mul R] [HasDistribNeg R] :
HasDistribNeg Rᵒᵈ
source
@[implicit_reducible]
instance OrderDual.instNonUnitalNonAssocRing {R : Type u_1} [NonUnitalNonAssocRing R] :
NonUnitalNonAssocRing Rᵒᵈ
source
@[implicit_reducible]
instance OrderDual.instNonUnitalRing {R : Type u_1} [NonUnitalRing R] :
NonUnitalRing Rᵒᵈ
source
@[implicit_reducible]
instance OrderDual.instNonAssocRing {R : Type u_1} [NonAssocRing R] :
NonAssocRing Rᵒᵈ
source
@[implicit_reducible]
instance OrderDual.instRing {R : Type u_1} [Ring R] :
Ring Rᵒᵈ
source
@[implicit_reducible]
instance OrderDual.instNonUnitalCommRing {R : Type u_1} [NonUnitalCommRing R] :
NonUnitalCommRing Rᵒᵈ
source
@[implicit_reducible]
instance OrderDual.instCommRing {R : Type u_1} [CommRing R] :
CommRing Rᵒᵈ
source
instance OrderDual.instIsDomain {R : Type u_1} [Ring R] [IsDomain R] :
IsDomain Rᵒᵈ
source
@[simp]
theorem toDual_natCast {R : Type u_1} [NatCast R] (n : ℕ) :
OrderDual.toDual ↑n = ↑n
source
@[simp]
theorem toDual_ofNat {R : Type u_1} [NatCast R] (n : ℕ) [n.AtLeastTwo] :
OrderDual.toDual (OfNat.ofNat n) = OfNat.ofNat n
source
@[simp]
theorem ofDual_natCast {R : Type u_1} [NatCast R] (n : ℕ) :
OrderDual.ofDual ↑n = ↑n
source
@[simp]
theorem ofDual_ofNat {R : Type u_1} [NatCast R] (n : ℕ) [n.AtLeastTwo] :
OrderDual.ofDual (OfNat.ofNat n) = OfNat.ofNat n
source
@[simp]
theorem toDual_intCast {R : Type u_1} [IntCast R] (n : ℤ) :
OrderDual.toDual ↑n = ↑n
source
@[simp]
theorem ofDual_intCast {R : Type u_1} [IntCast R] (n : ℤ) :
OrderDual.ofDual ↑n = ↑n

Lexicographical order #

source
@[implicit_reducible]
instance Lex.instDistrib {R : Type u_1} [Distrib R] :
Distrib (Lex R)
source
instance Lex.instLeftDistribClass {R : Type u_1} [Mul R] [Add R] [LeftDistribClass R] :
LeftDistribClass (Lex R)
source
instance Lex.instRightDistribClass {R : Type u_1} [Mul R] [Add R] [RightDistribClass R] :
RightDistribClass (Lex R)
source
@[implicit_reducible]
instance Lex.instNonUnitalNonAssocSemiring {R : Type u_1} [NonUnitalNonAssocSemiring R] :
NonUnitalNonAssocSemiring (Lex R)
source
@[implicit_reducible]
instance Lex.instNonUnitalSemiring {R : Type u_1} [NonUnitalSemiring R] :
NonUnitalSemiring (Lex R)
source
@[implicit_reducible]
instance Lex.instNatCast {R : Type u_1} [NatCast R] :
NatCast (Lex R)
source
@[implicit_reducible]
instance Lex.instIntCast {R : Type u_1} [IntCast R] :
IntCast (Lex R)
source
@[implicit_reducible]
instance Lex.instAddMonoidWithOne {R : Type u_1} [AddMonoidWithOne R] :
AddMonoidWithOne (Lex R)
source
@[implicit_reducible]
instance Lex.instAddCommMonoidWithOne {R : Type u_1} [AddCommMonoidWithOne R] :
AddCommMonoidWithOne (Lex R)
source
@[implicit_reducible]
instance Lex.instAddGroupWithOne {R : Type u_1} [AddGroupWithOne R] :
AddGroupWithOne (Lex R)
source
@[implicit_reducible]
instance Lex.instAddCommGroupWithOne {R : Type u_1} [AddCommGroupWithOne R] :
AddCommGroupWithOne (Lex R)
source
@[implicit_reducible]
instance Lex.instNonAssocSemiring {R : Type u_1} [NonAssocSemiring R] :
NonAssocSemiring (Lex R)
source
@[implicit_reducible]
instance Lex.instSemiring {R : Type u_1} [Semiring R] :
Semiring (Lex R)
source
@[implicit_reducible]
instance Lex.instNonUnitalCommSemiring {R : Type u_1} [NonUnitalCommSemiring R] :
NonUnitalCommSemiring (Lex R)
source
@[implicit_reducible]
instance Lex.instCommSemiring {R : Type u_1} [CommSemiring R] :
CommSemiring (Lex R)
source
@[implicit_reducible]
instance Lex.instHasDistribNeg {R : Type u_1} [Mul R] [HasDistribNeg R] :
HasDistribNeg (Lex R)
source
@[implicit_reducible]
instance Lex.instNonUnitalNonAssocRing {R : Type u_1} [NonUnitalNonAssocRing R] :
NonUnitalNonAssocRing (Lex R)
source
@[implicit_reducible]
instance Lex.instNonUnitalRing {R : Type u_1} [NonUnitalRing R] :
NonUnitalRing (Lex R)
source
@[implicit_reducible]
instance Lex.instNonAssocRing {R : Type u_1} [NonAssocRing R] :
NonAssocRing (Lex R)
source
@[implicit_reducible]
instance Lex.instRing {R : Type u_1} [Ring R] :
Ring (Lex R)
source
@[implicit_reducible]
instance Lex.instNonUnitalCommRing {R : Type u_1} [NonUnitalCommRing R] :
NonUnitalCommRing (Lex R)
source
@[implicit_reducible]
instance Lex.instCommRing {R : Type u_1} [CommRing R] :
CommRing (Lex R)
source
instance Lex.instIsDomain {R : Type u_1} [Ring R] [IsDomain R] :
IsDomain (Lex R)
source
@[simp]
theorem toLex_natCast {R : Type u_1} [NatCast R] (n : ℕ) :
toLex ↑n = ↑n
source
@[simp]
theorem toLex_ofNat {R : Type u_1} [NatCast R] (n : ℕ) [n.AtLeastTwo] :
toLex (OfNat.ofNat n) = OfNat.ofNat n
source
@[simp]
theorem ofLex_natCast {R : Type u_1} [NatCast R] (n : ℕ) :
ofLex ↑n = ↑n
source
@[simp]
theorem ofLex_ofNat {R : Type u_1} [NatCast R] (n : ℕ) [n.AtLeastTwo] :
ofLex (OfNat.ofNat n) = OfNat.ofNat n
source
@[simp]
theorem toLex_intCast {R : Type u_1} [IntCast R] (n : ℤ) :
toLex ↑n = ↑n
source
@[simp]
theorem ofLex_intCast {R : Type u_1} [IntCast R] (n : ℤ) :
ofLex ↑n = ↑n