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ᵒᵈ

Equations

• OrderDual.instDistrib = { toMul := OrderDual.instMul, toAdd := OrderDual.instAdd, left_distrib := ⋯, right_distrib := ⋯ }

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ᵒᵈ

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

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

Equations

• OrderDual.instNatCast = h

@[implicit_reducible]

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

Equations

• OrderDual.instIntCast = h

@[implicit_reducible]

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

Equations

• OrderDual.instAddMonoidWithOne = { toNatCast := OrderDual.instNatCast, toAddMonoid := OrderDual.instAddMonoid, toOne := OrderDual.instOne, natCast_zero := ⋯, natCast_succ := ⋯ }

@[implicit_reducible]

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

Equations

• OrderDual.instAddCommMonoidWithOne = { toAddMonoidWithOne := OrderDual.instAddMonoidWithOne, add_comm := ⋯ }

@[implicit_reducible]

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

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

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

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

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

Equations

• OrderDual.instNonUnitalSemiring = { toNonUnitalNonAssocSemiring := OrderDual.instNonUnitalNonAssocSemiring, mul_assoc := ⋯ }

@[implicit_reducible]

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

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

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

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

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

Equations

• OrderDual.instNonUnitalCommSemiring = { toNonUnitalSemiring := OrderDual.instNonUnitalSemiring, mul_comm := ⋯ }

@[implicit_reducible]

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

Equations

• OrderDual.instCommSemiring = { toSemiring := OrderDual.instSemiring, mul_comm := ⋯ }

@[implicit_reducible]

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

Equations

• OrderDual.instHasDistribNeg = { toInvolutiveNeg := OrderDual.instInvolutiveNeg, neg_mul := ⋯, mul_neg := ⋯ }

@[implicit_reducible]

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

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

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

Equations

• OrderDual.instNonUnitalRing = { toNonUnitalNonAssocRing := OrderDual.instNonUnitalNonAssocRing, mul_assoc := ⋯ }

@[implicit_reducible]

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

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

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

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

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

Equations

• OrderDual.instNonUnitalCommRing = { toNonUnitalRing := OrderDual.instNonUnitalRing, mul_comm := ⋯ }

@[implicit_reducible]

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

Equations

• OrderDual.instCommRing = { toRing := OrderDual.instRing, mul_comm := ⋯ }

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)

Equations

• instDistribLex = h

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)

Equations

• instNonUnitalNonAssocSemiringLex = h

@[implicit_reducible]

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

Equations

• instNonUnitalSemiringLex = h

@[implicit_reducible]

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

Equations

• instNonAssocSemiringLex = h

@[implicit_reducible]

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

Equations

• instSemiringLex = h

@[implicit_reducible]

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

Equations

• instNonUnitalCommSemiringLex = h

@[implicit_reducible]

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

Equations

• instCommSemiringLex = h

@[implicit_reducible]

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

Equations

• instHasDistribNegLex = h

@[implicit_reducible]

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

Equations

• instNonUnitalNonAssocRingLex = h

@[implicit_reducible]

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

Equations

• instNonUnitalRingLex = h

@[implicit_reducible]

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

Equations

• instNonAssocRingLex = h

@[implicit_reducible]

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

Equations

• instRingLex = h

@[implicit_reducible]

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

Equations

• instNonUnitalCommRingLex = h

@[implicit_reducible]

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

Equations

• instCommRingLex = h

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