Successor and predecessor on type tags

This file declates successor and predecessor orders on type tags.

instance instSuccOrderMultiplicative {X : Type u_1} [Preorder X] [h : SuccOrder X] : SuccOrder (Multiplicative X)

Equations

• instSuccOrderMultiplicative = h

instance instSuccOrderAdditive {X : Type u_1} [Preorder X] [h : SuccOrder X] : SuccOrder (Additive X)

Equations

• instSuccOrderAdditive = h

instance instPredOrderMultiplicative {X : Type u_1} [Preorder X] [h : PredOrder X] : PredOrder (Multiplicative X)

Equations

• instPredOrderMultiplicative = h

instance instPredOrderAdditive {X : Type u_1} [Preorder X] [h : PredOrder X] : PredOrder (Additive X)

Equations

• instPredOrderAdditive = h

instance instIsSuccArchimedeanMultiplicative {X : Type u_1} [Preorder X] [SuccOrder X] [h : IsSuccArchimedean X] : IsSuccArchimedean (Multiplicative X)

Equations

• ⋯ = h

instance instIsSuccArchimedeanAdditive {X : Type u_1} [Preorder X] [SuccOrder X] [h : IsSuccArchimedean X] : IsSuccArchimedean (Additive X)

Equations

• ⋯ = h

instance instIsPredArchimedeanMultiplicative {X : Type u_1} [Preorder X] [PredOrder X] [h : IsPredArchimedean X] : IsPredArchimedean (Multiplicative X)

Equations

• ⋯ = h

instance instIsPredArchimedeanAdditive {X : Type u_1} [Preorder X] [PredOrder X] [h : IsPredArchimedean X] : IsPredArchimedean (Additive X)

Equations

• ⋯ = h

@[simp]

theorem Order.succ_ofMul {X : Type u_1} [Preorder X] [SuccOrder X] (x : X) : Order.succ (Additive.ofMul x) = Additive.ofMul (Order.succ x)

@[simp]

theorem Order.succ_toMul {X : Type u_1} [Preorder X] [SuccOrder X] (x : X) : Order.succ (Additive.toMul x) = Additive.toMul (Order.succ x)

@[simp]

theorem Order.succ_ofAdd {X : Type u_1} [Preorder X] [SuccOrder X] (x : X) : Order.succ (Multiplicative.ofAdd x) = Multiplicative.ofAdd (Order.succ x)

@[simp]

theorem Order.succ_toAdd {X : Type u_1} [Preorder X] [SuccOrder X] (x : X) : Order.succ (Multiplicative.toAdd x) = Multiplicative.toAdd (Order.succ x)

@[simp]

theorem Order.pred_ofMul {X : Type u_1} [Preorder X] [PredOrder X] (x : X) : Order.pred (Additive.ofMul x) = Additive.ofMul (Order.pred x)

@[simp]

theorem Order.pred_toMul {X : Type u_1} [Preorder X] [PredOrder X] (x : X) : Order.pred (Additive.toMul x) = Additive.toMul (Order.pred x)

@[simp]

theorem Order.pred_ofAdd {X : Type u_1} [Preorder X] [PredOrder X] (x : X) : Order.pred (Multiplicative.ofAdd x) = Multiplicative.ofAdd (Order.pred x)

@[simp]

theorem Order.pred_toAdd {X : Type u_1} [Preorder X] [PredOrder X] (x : X) : Order.pred (Multiplicative.toAdd x) = Multiplicative.toAdd (Order.pred x)