Ring structure on the order type synonyms

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

Order dual

@[implicit_reducible]

instance OrderDual.instDistrib {R : Type u_1} [h : Distrib R] : Distrib Rᵒᵈ

instance OrderDual.instLeftDistribClass {R : Type u_1} [Mul R] [Add R] [h : LeftDistribClass R] : LeftDistribClass Rᵒᵈ

instance OrderDual.instRightDistribClass {R : Type u_1} [Mul R] [Add R] [h : RightDistribClass R] : RightDistribClass Rᵒᵈ

@[implicit_reducible]

instance OrderDual.instNonUnitalNonAssocSemiring {R : Type u_1} [h : NonUnitalNonAssocSemiring R] : NonUnitalNonAssocSemiring Rᵒᵈ

@[implicit_reducible]

instance OrderDual.instNatCast {R : Type u_1} [h : NatCast R] : NatCast Rᵒᵈ

@[implicit_reducible]

instance OrderDual.instIntCast {R : Type u_1} [h : IntCast R] : IntCast Rᵒᵈ

@[implicit_reducible]

instance OrderDual.instAddMonoidWithOne {R : Type u_1} [h : AddMonoidWithOne R] : AddMonoidWithOne Rᵒᵈ

@[implicit_reducible]

instance OrderDual.instAddCommMonoidWithOne {R : Type u_1} [h : AddCommMonoidWithOne R] : AddCommMonoidWithOne Rᵒᵈ

@[implicit_reducible]

instance OrderDual.instAddGroupWithOne {R : Type u_1} [h : AddGroupWithOne R] : AddGroupWithOne Rᵒᵈ

@[implicit_reducible]

instance OrderDual.instAddCommGroupWithOne {R : Type u_1} [AddCommGroupWithOne R] : AddCommGroupWithOne Rᵒᵈ

@[implicit_reducible]

instance OrderDual.instNonUnitalSemiring {R : Type u_1} [h : NonUnitalSemiring R] : NonUnitalSemiring Rᵒᵈ

@[implicit_reducible]

instance OrderDual.instNonAssocSemiring {R : Type u_1} [h : NonAssocSemiring R] : NonAssocSemiring Rᵒᵈ

@[implicit_reducible]

instance OrderDual.instSemiring {R : Type u_1} [h : Semiring R] : Semiring Rᵒᵈ

@[implicit_reducible]

instance OrderDual.instNonUnitalCommSemiring {R : Type u_1} [h : NonUnitalCommSemiring R] : NonUnitalCommSemiring Rᵒᵈ

@[implicit_reducible]

instance OrderDual.instCommSemiring {R : Type u_1} [h : CommSemiring R] : CommSemiring Rᵒᵈ

@[implicit_reducible]

instance OrderDual.instHasDistribNeg {R : Type u_1} [Mul R] [h : HasDistribNeg R] : HasDistribNeg Rᵒᵈ

@[implicit_reducible]

instance OrderDual.instNonUnitalNonAssocRing {R : Type u_1} [h : NonUnitalNonAssocRing R] : NonUnitalNonAssocRing Rᵒᵈ

@[implicit_reducible]

instance OrderDual.instNonUnitalRing {R : Type u_1} [h : NonUnitalRing R] : NonUnitalRing Rᵒᵈ

@[implicit_reducible]

instance OrderDual.instNonAssocRing {R : Type u_1} [h : NonAssocRing R] : NonAssocRing Rᵒᵈ

@[implicit_reducible]

instance OrderDual.instRing {R : Type u_1} [h : Ring R] : Ring Rᵒᵈ

@[implicit_reducible]

instance OrderDual.instNonUnitalCommRing {R : Type u_1} [h : NonUnitalCommRing R] : NonUnitalCommRing Rᵒᵈ

@[implicit_reducible]

instance OrderDual.instCommRing {R : Type u_1} [h : CommRing R] : CommRing Rᵒᵈ

instance OrderDual.instIsDomain {R : Type u_1} [Ring R] [h : IsDomain R] : IsDomain Rᵒᵈ

@[simp]

theorem toDual_natCast {R : Type u_1} [NatCast R] (n : ℕ) : OrderDual.toDual ↑n = ↑n

@[simp]

theorem toDual_ofNat {R : Type u_1} [NatCast R] (n : ℕ) [n.AtLeastTwo] : OrderDual.toDual (OfNat.ofNat n) = OfNat.ofNat n

@[simp]

theorem ofDual_natCast {R : Type u_1} [NatCast R] (n : ℕ) : OrderDual.ofDual ↑n = ↑n

@[simp]

theorem ofDual_ofNat {R : Type u_1} [NatCast R] (n : ℕ) [n.AtLeastTwo] : OrderDual.ofDual (OfNat.ofNat n) = OfNat.ofNat n

@[simp]

theorem toDual_intCast {R : Type u_1} [IntCast R] (n : ℤ) : OrderDual.toDual ↑n = ↑n

@[simp]

theorem ofDual_intCast {R : Type u_1} [IntCast R] (n : ℤ) : OrderDual.ofDual ↑n = ↑n

Lexicographical order

@[implicit_reducible]

instance instDistribLex {R : Type u_1} [h : Distrib R] : Distrib (Lex R)

instance instLeftDistribClassLex {R : Type u_1} [Mul R] [Add R] [h : LeftDistribClass R] : LeftDistribClass (Lex R)

instance instRightDistribClassLex {R : Type u_1} [Mul R] [Add R] [h : RightDistribClass R] : RightDistribClass (Lex R)

@[implicit_reducible]

instance instNonUnitalNonAssocSemiringLex {R : Type u_1} [h : NonUnitalNonAssocSemiring R] : NonUnitalNonAssocSemiring (Lex R)

@[implicit_reducible]

instance instNonUnitalSemiringLex {R : Type u_1} [h : NonUnitalSemiring R] : NonUnitalSemiring (Lex R)

@[implicit_reducible]

instance instNonAssocSemiringLex {R : Type u_1} [h : NonAssocSemiring R] : NonAssocSemiring (Lex R)

@[implicit_reducible]

instance instSemiringLex {R : Type u_1} [h : Semiring R] : Semiring (Lex R)

@[implicit_reducible]

instance instNonUnitalCommSemiringLex {R : Type u_1} [h : NonUnitalCommSemiring R] : NonUnitalCommSemiring (Lex R)

@[implicit_reducible]

instance instCommSemiringLex {R : Type u_1} [h : CommSemiring R] : CommSemiring (Lex R)

@[implicit_reducible]

instance instHasDistribNegLex {R : Type u_1} [Mul R] [h : HasDistribNeg R] : HasDistribNeg (Lex R)

@[implicit_reducible]

instance instNonUnitalNonAssocRingLex {R : Type u_1} [h : NonUnitalNonAssocRing R] : NonUnitalNonAssocRing (Lex R)

@[implicit_reducible]

instance instNonUnitalRingLex {R : Type u_1} [h : NonUnitalRing R] : NonUnitalRing (Lex R)

@[implicit_reducible]

instance instNonAssocRingLex {R : Type u_1} [h : NonAssocRing R] : NonAssocRing (Lex R)

@[implicit_reducible]

instance instRingLex {R : Type u_1} [h : Ring R] : Ring (Lex R)

@[implicit_reducible]

instance instNonUnitalCommRingLex {R : Type u_1} [h : NonUnitalCommRing R] : NonUnitalCommRing (Lex R)

@[implicit_reducible]

instance instCommRingLex {R : Type u_1} [h : CommRing R] : CommRing (Lex R)

instance instIsDomainLex {R : Type u_1} [Ring R] [h : IsDomain R] : IsDomain (Lex R)