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} [h : Distrib R] :
Distrib Rᵒᵈ
source
instance OrderDual.instLeftDistribClass {R : Type u_1} [Mul R] [Add R] [h : LeftDistribClass R] :
LeftDistribClass Rᵒᵈ
source
instance OrderDual.instRightDistribClass {R : Type u_1} [Mul R] [Add R] [h : RightDistribClass R] :
RightDistribClass Rᵒᵈ
source
@[implicit_reducible]
instance OrderDual.instNonUnitalNonAssocSemiring {R : Type u_1} [h : NonUnitalNonAssocSemiring R] :
NonUnitalNonAssocSemiring Rᵒᵈ
source
@[implicit_reducible]
instance OrderDual.instNatCast {R : Type u_1} [h : NatCast R] :
NatCast Rᵒᵈ
source
@[implicit_reducible]
instance OrderDual.instIntCast {R : Type u_1} [h : IntCast R] :
IntCast Rᵒᵈ
source
@[implicit_reducible]
instance OrderDual.instAddMonoidWithOne {R : Type u_1} [h : AddMonoidWithOne R] :
AddMonoidWithOne Rᵒᵈ
source
@[implicit_reducible]
instance OrderDual.instAddCommMonoidWithOne {R : Type u_1} [h : AddCommMonoidWithOne R] :
AddCommMonoidWithOne Rᵒᵈ
source
@[implicit_reducible]
instance OrderDual.instAddGroupWithOne {R : Type u_1} [h : 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} [h : NonUnitalSemiring R] :
NonUnitalSemiring Rᵒᵈ
source
@[implicit_reducible]
instance OrderDual.instNonAssocSemiring {R : Type u_1} [h : NonAssocSemiring R] :
NonAssocSemiring Rᵒᵈ
source
@[implicit_reducible]
instance OrderDual.instSemiring {R : Type u_1} [h : Semiring R] :
Semiring Rᵒᵈ
source
@[implicit_reducible]
instance OrderDual.instNonUnitalCommSemiring {R : Type u_1} [h : NonUnitalCommSemiring R] :
NonUnitalCommSemiring Rᵒᵈ
source
@[implicit_reducible]
instance OrderDual.instCommSemiring {R : Type u_1} [h : CommSemiring R] :
CommSemiring Rᵒᵈ
source
@[implicit_reducible]
instance OrderDual.instHasDistribNeg {R : Type u_1} [Mul R] [h : HasDistribNeg R] :
HasDistribNeg Rᵒᵈ
source
@[implicit_reducible]
instance OrderDual.instNonUnitalNonAssocRing {R : Type u_1} [h : NonUnitalNonAssocRing R] :
NonUnitalNonAssocRing Rᵒᵈ
source
@[implicit_reducible]
instance OrderDual.instNonUnitalRing {R : Type u_1} [h : NonUnitalRing R] :
NonUnitalRing Rᵒᵈ
source
@[implicit_reducible]
instance OrderDual.instNonAssocRing {R : Type u_1} [h : NonAssocRing R] :
NonAssocRing Rᵒᵈ
source
@[implicit_reducible]
instance OrderDual.instRing {R : Type u_1} [h : Ring R] :
Ring Rᵒᵈ
source
@[implicit_reducible]
instance OrderDual.instNonUnitalCommRing {R : Type u_1} [h : NonUnitalCommRing R] :
NonUnitalCommRing Rᵒᵈ
source
@[implicit_reducible]
instance OrderDual.instCommRing {R : Type u_1} [h : CommRing R] :
CommRing Rᵒᵈ
source
instance OrderDual.instIsDomain {R : Type u_1} [Ring R] [h : 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 instDistribLex {R : Type u_1} [h : Distrib R] :
Distrib (Lex R)
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
@[implicit_reducible]
instance instNonUnitalNonAssocSemiringLex {R : Type u_1} [h : NonUnitalNonAssocSemiring R] :
NonUnitalNonAssocSemiring (Lex R)
source
@[implicit_reducible]
instance instNonUnitalSemiringLex {R : Type u_1} [h : NonUnitalSemiring R] :
NonUnitalSemiring (Lex R)
source
@[implicit_reducible]
instance instNonAssocSemiringLex {R : Type u_1} [h : NonAssocSemiring R] :
NonAssocSemiring (Lex R)
source
@[implicit_reducible]
instance instSemiringLex {R : Type u_1} [h : Semiring R] :
Semiring (Lex R)
source
@[implicit_reducible]
instance instNonUnitalCommSemiringLex {R : Type u_1} [h : NonUnitalCommSemiring R] :
NonUnitalCommSemiring (Lex R)
source
@[implicit_reducible]
instance instCommSemiringLex {R : Type u_1} [h : CommSemiring R] :
CommSemiring (Lex R)
source
@[implicit_reducible]
instance instHasDistribNegLex {R : Type u_1} [Mul R] [h : HasDistribNeg R] :
HasDistribNeg (Lex R)
source
@[implicit_reducible]
instance instNonUnitalNonAssocRingLex {R : Type u_1} [h : NonUnitalNonAssocRing R] :
NonUnitalNonAssocRing (Lex R)
source
@[implicit_reducible]
instance instNonUnitalRingLex {R : Type u_1} [h : NonUnitalRing R] :
NonUnitalRing (Lex R)
source
@[implicit_reducible]
instance instNonAssocRingLex {R : Type u_1} [h : NonAssocRing R] :
NonAssocRing (Lex R)
source
@[implicit_reducible]
instance instRingLex {R : Type u_1} [h : Ring R] :
Ring (Lex R)
source
@[implicit_reducible]
instance instNonUnitalCommRingLex {R : Type u_1} [h : NonUnitalCommRing R] :
NonUnitalCommRing (Lex R)
source
@[implicit_reducible]
instance instCommRingLex {R : Type u_1} [h : CommRing R] :
CommRing (Lex R)
source
instance instIsDomainLex {R : Type u_1} [Ring R] [h : IsDomain R] :
IsDomain (Lex R)