Successor and predecessor on type tags

This file declares successor and predecessor orders on type tags.

@[implicit_reducible]

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

Equations

• instSuccOrderMultiplicative = h

@[implicit_reducible]

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

Equations

• instSuccOrderAdditive = h

@[implicit_reducible]

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

Equations

• instPredOrderMultiplicative = h

@[implicit_reducible]

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)

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

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

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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