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} [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] [LeftDistribClass R] : LeftDistribClass Rᵒᵈ

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

@[implicit_reducible]

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

Equations

• OrderDual.instNonUnitalNonAssocSemiring = { toAddCommMonoid := OrderDual.instAddCommMonoid, toMul := OrderDual.instMul, left_distrib := ⋯, right_distrib := ⋯, zero_mul := ⋯, mul_zero := ⋯ }

@[implicit_reducible]

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

Equations

• OrderDual.instNatCast = OrderDual.instNatCast._aux_1

@[implicit_reducible]

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

Equations

• OrderDual.instIntCast = OrderDual.instIntCast._aux_1

@[implicit_reducible]

instance OrderDual.instAddMonoidWithOne {R : Type u_1} [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} [AddCommMonoidWithOne R] : AddCommMonoidWithOne Rᵒᵈ

Equations

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

@[implicit_reducible]

instance OrderDual.instAddGroupWithOne {R : Type u_1} [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} [NonUnitalSemiring R] : NonUnitalSemiring Rᵒᵈ

Equations

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

@[implicit_reducible]

instance OrderDual.instNonAssocSemiring {R : Type u_1} [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} [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} [NonUnitalCommSemiring R] : NonUnitalCommSemiring Rᵒᵈ

Equations

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

@[implicit_reducible]

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

Equations

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

@[implicit_reducible]

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

Equations

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

@[implicit_reducible]

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

Equations

• OrderDual.instNonUnitalNonAssocRing = { toAddCommGroup := OrderDual.instAddCommGroup, toMul := OrderDual.instMul, left_distrib := ⋯, right_distrib := ⋯, zero_mul := ⋯, mul_zero := ⋯ }

@[implicit_reducible]

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

Equations

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

@[implicit_reducible]

instance OrderDual.instNonAssocRing {R : Type u_1} [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} [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} [NonUnitalCommRing R] : NonUnitalCommRing Rᵒᵈ

Equations

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

@[implicit_reducible]

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

Equations

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

instance OrderDual.instIsDomain {R : Type u_1} [Ring R] [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 Lex.instDistrib {R : Type u_1} [Distrib R] : Distrib (Lex R)

Equations

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

instance Lex.instLeftDistribClass {R : Type u_1} [Mul R] [Add R] [LeftDistribClass R] : LeftDistribClass (Lex R)

instance Lex.instRightDistribClass {R : Type u_1} [Mul R] [Add R] [RightDistribClass R] : RightDistribClass (Lex R)

@[implicit_reducible]

instance Lex.instNonUnitalNonAssocSemiring {R : Type u_1} [NonUnitalNonAssocSemiring R] : NonUnitalNonAssocSemiring (Lex R)

Equations

• Lex.instNonUnitalNonAssocSemiring = { toAddCommMonoid := Lex.instAddCommMonoid, toMul := Lex.instMul, left_distrib := ⋯, right_distrib := ⋯, zero_mul := ⋯, mul_zero := ⋯ }

@[implicit_reducible]

instance Lex.instNonUnitalSemiring {R : Type u_1} [NonUnitalSemiring R] : NonUnitalSemiring (Lex R)

Equations

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

@[implicit_reducible]

instance Lex.instNatCast {R : Type u_1} [NatCast R] : NatCast (Lex R)

Equations

• Lex.instNatCast = Lex.instNatCast._aux_1

@[implicit_reducible]

instance Lex.instIntCast {R : Type u_1} [IntCast R] : IntCast (Lex R)

Equations

• Lex.instIntCast = Lex.instIntCast._aux_1

@[implicit_reducible]

instance Lex.instAddMonoidWithOne {R : Type u_1} [AddMonoidWithOne R] : AddMonoidWithOne (Lex R)

Equations

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

@[implicit_reducible]

instance Lex.instAddCommMonoidWithOne {R : Type u_1} [AddCommMonoidWithOne R] : AddCommMonoidWithOne (Lex R)

Equations

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

@[implicit_reducible]

instance Lex.instAddGroupWithOne {R : Type u_1} [AddGroupWithOne R] : AddGroupWithOne (Lex R)

Equations

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

@[implicit_reducible]

instance Lex.instAddCommGroupWithOne {R : Type u_1} [AddCommGroupWithOne R] : AddCommGroupWithOne (Lex R)

Equations

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

@[implicit_reducible]

instance Lex.instNonAssocSemiring {R : Type u_1} [NonAssocSemiring R] : NonAssocSemiring (Lex R)

Equations

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

@[implicit_reducible]

instance Lex.instSemiring {R : Type u_1} [Semiring R] : Semiring (Lex R)

Equations

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

@[implicit_reducible]

instance Lex.instNonUnitalCommSemiring {R : Type u_1} [NonUnitalCommSemiring R] : NonUnitalCommSemiring (Lex R)

Equations

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

@[implicit_reducible]

instance Lex.instCommSemiring {R : Type u_1} [CommSemiring R] : CommSemiring (Lex R)

Equations

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

@[implicit_reducible]

instance Lex.instHasDistribNeg {R : Type u_1} [Mul R] [HasDistribNeg R] : HasDistribNeg (Lex R)

Equations

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

@[implicit_reducible]

instance Lex.instNonUnitalNonAssocRing {R : Type u_1} [NonUnitalNonAssocRing R] : NonUnitalNonAssocRing (Lex R)

Equations

• Lex.instNonUnitalNonAssocRing = { toAddCommGroup := Lex.instAddCommGroup, toMul := Lex.instMul, left_distrib := ⋯, right_distrib := ⋯, zero_mul := ⋯, mul_zero := ⋯ }

@[implicit_reducible]

instance Lex.instNonUnitalRing {R : Type u_1} [NonUnitalRing R] : NonUnitalRing (Lex R)

Equations

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

@[implicit_reducible]

instance Lex.instNonAssocRing {R : Type u_1} [NonAssocRing R] : NonAssocRing (Lex R)

Equations

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

@[implicit_reducible]

instance Lex.instRing {R : Type u_1} [Ring R] : Ring (Lex R)

Equations

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

@[implicit_reducible]

instance Lex.instNonUnitalCommRing {R : Type u_1} [NonUnitalCommRing R] : NonUnitalCommRing (Lex R)

Equations

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

@[implicit_reducible]

instance Lex.instCommRing {R : Type u_1} [CommRing R] : CommRing (Lex R)

Equations

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

instance Lex.instIsDomain {R : Type u_1} [Ring R] [IsDomain R] : IsDomain (Lex R)

@[simp]

theorem toLex_natCast {R : Type u_1} [NatCast R] (n : ℕ) : toLex ↑n = ↑n

@[simp]

theorem toLex_ofNat {R : Type u_1} [NatCast R] (n : ℕ) [n.AtLeastTwo] : toLex (OfNat.ofNat n) = OfNat.ofNat n

@[simp]

theorem ofLex_natCast {R : Type u_1} [NatCast R] (n : ℕ) : ofLex ↑n = ↑n

@[simp]

theorem ofLex_ofNat {R : Type u_1} [NatCast R] (n : ℕ) [n.AtLeastTwo] : ofLex (OfNat.ofNat n) = OfNat.ofNat n

@[simp]

theorem toLex_intCast {R : Type u_1} [IntCast R] (n : ℤ) : toLex ↑n = ↑n

@[simp]

theorem ofLex_intCast {R : Type u_1} [IntCast R] (n : ℤ) : ofLex ↑n = ↑n